Re: [mizar] Mizar grammar up to date?

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

On Thu, 19 Dec 2002, Markus Moschner wrote:

> Just noticed that Mizar does not allow
> Structure-definitions outside Definitions -example A: 
> (I know,that is an incomplete induction, but is irrelevant now!-).
> But the grammar from Mizar Web pages still allows - example B.

It seems so. The consistency of the formal grammar and the
implementation is not checked in any automated way now. Perhaps all of the 
Mizar2XML projects (:-) will fix this by providing uptodate DTD, that can 
be automatically exported to BNF.

Regards,
Josef