Re: [mizar] vocabularies

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Andrzej,

>It is true, that the names of vocabularies are (mostly)
>the same as the names of articles.

Precisely.  So making those names _exactly_ correspond
seems a very minor change to me.

>I cannot imagine how we could maintain MML with the
>vocabularies glued in the articles.

Why not?  Instead of having two files foo.voc and foo.miz
you would have one, but why does it matter how things are
distributed over _files?_  And if you do _not_ want to make
the names match up exactly, you could have dummy articles
that _just_ have a vocabulary.

I don't see the problem, sorry.  It is trivial to write a
perl script that transforms a directory with separate .voc
and .miz files into a directory in which the vocabularies
are in included in the .miz files.  So to "maintain" MML
one then could run that script, do whatever is needed for
maintenance, and then run the inverse script.

But I don't see why for maintenance the vocabularies couldn't
stay in the .miz files.  Can you explain?

Freek