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

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

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