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