Re: vocabularies

Josef Urban <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]> 
Hi Freek,

On Mon, 5 Jan 2009, Freek Wiedijk wrote:

> Hi Josef,
>
> A happy new year!

Happy New Year!
(But I really wonder if such greetings belong to globalised fora: e.g. 
Jews consider Christmas a pagan ritual :-)

>> How about removing the "vocabularies" directive
>> completely? The "notations" would say to the parser which
>> symbols are available.
>
> 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".

Josef
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.