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

Josef Urban wrote:

>
> This is written in Jesse's e-mail: the metadata could be processed by
> standard Mizar-based tools that are currently used for creating the
> HTML representation, are (going to be) used for collecting data for
> MML Query, and possibly also other things like FM and MPTP. 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.
>
'natural' ?

Well, if you mean by an 'article' a mathematical paper you're right, if
it is thought as a script for the verifier, you're not.

Regards,
Andrzej