[mizar] Mizar grammar up to date?

[Markus Moschner <moschm@ags.uni-sb.de>]

Dear All!

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.

Are there other known features?

Example A: 
::definition
 struct(RelStr) OrthoRelStr
::>   *391
     (# carrier -> set,
        InternalRel -> (Relation of the carrier),
        Compl -> UnOp of the carrier #);
::end;
::> 391: Incorrect beginning of a text item

Example B:
Text Item


Syntax

 Text-Item   =   
  
     Reservation   |   
     Definitional-Item   |   
     Structure-Definition   |   
     Theorem   |   
     Scheme   |   
     Auxiliary-Item   |   
     Canceled-Theorem   .



        Best regards,
             Markus Moschner