Re: vocabularies

Freek Wiedijk <[email protected]> Mon, 5 Jan 2009 15:38:10 +0100

Newsgroups	gmane.comp.mathematics.mizar
Message-ID	<[email protected]>

Hi Josef,

A happy new year!

>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?

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.