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.