Josef Urban wrote:
The difference is in reconstructing the article in HTML. The syntax in comments allows users to do stupid things like:theorem Foo a+b = ::?SECTION Blah b+a proof ... end;It is easy for the Mizar parser to disallow this stupidity. It is not easy for a lightweight parser which is not aware of the standard Mizar syntax.
A good argument. The place of this pragma must be controlled. Perhaps some others, too. Does it mean
that we should introduce a reserved word for it? section XXXX;It results in an advantage for the parser: better reporting of errors. E.g. reporting unpaired 'proof'.
Merry Christmass, Andrzej