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

Josef Urban <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>

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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.