Re: [mizar] vocabularies

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

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