Re: vocabularies

Freek Wiedijk <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.