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

On Wed, 26 Nov 2008, trybulec wrote:

>> I suggest, following Jesse's suggestion that the entire .bib files for
>> Mizar articles be incorporated into the .miz files.
>>
>>
> I am not against, I am not pro.  Could me tell me what would be the gain,
> if we did it?

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.

Josef