Re: [mizar] an extension of the mizar language for dealing with article metadata

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

Josef:

>It is not practical to keep these data separately and
>process them by separate tools, especially when they are
>quite a natural part of the articles.

Why not?  The vocabulary files are exactly like that too.

Of course _I_ always want the vocabulary files to be part
of the articles.  It is a pain that they have their own
name space, and that you need two files instead of one.

However, "not practical" seems too strong.

Freek