Re: [mizar] vocabularies

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>>To me this seems a much more drastic change than what I
>>was proposing.  I guess it also would mean unifying the
>>vocabulary and article name spaces?
>
>I think there would be no "vocabulary".

So all vocabularies would be always active?  But then I
could break existing articles by introducing new symbols
in my vocabulary to MML.  So how should I test for that?

Or would you want to introduce the vocabulary elements
together with the notation, always?  So that sounds a more
radical change than what I proposed.  (My proposal was
just to move text from one file to another, but without
the system really changing.)

Freek