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

Josef Urban wrote:

>
> So why is the keyword "begin" allowed multiple times to introduce 
> sections, and why do all articles start with the standard header 
> containing author and title, why are comments allowed at all? If there 
> is no need to process and present these article

That is my complaint, the repetition of 'begin' has nothing to do with 
Mizar, and should not be allowed. I would prefer
something like:

::$ SECTION

maybe with a name, as a cross reference to the place where description 
of the section is kept:
   the title, maybe a summary

BTW. In Mizar HPF (around 1993) only one kind of comments was allowed: 
written by a pen on the printout.
It did not work.

Regards,
Andrzej