[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] vocabularies



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