[mizar] Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi All,

I think that the following two production rules in the current grammar
( http://mmlquery.mizar.org/mmlquery/mizar-grammar.xml )
must be changed:

-------------------------------------------------------------------------------
From:

Definitional-Block =
	"definition" { ( Definition-Item | Definition ) } [ Redefinition-Block ] 
"end" .

To:

Definitional-Block =
	"definition" { ( Definition-Item | Definition ) } { Redefinition-Block } 
"end" .

Justification: the following fragment from MML.
  subset_1.miz: lines 223 - 263.
-------------------------------
definition let E,A;
  func A` -> Subset of E equals  E \ A;
  ...
  redefine func A \/ B -> Subset of E;
  ...
  redefine func A \+\ B -> Subset of E;
  ...
 end;
-------------------------------

-------------------------------------------------------------------------------

From:

Attribute-Definition =
	"attr" Attribute-Pattern "means" Definiens ";" [ "correctness" Justification 
";" ] .

To:

Attribute-Definition =
	"attr" Attribute-Pattern "means" Definiens ";" Correctness-Conditions .

Justification: the following fragment from MML.
  funct_1.miz: lines 2137 - 2156.
-------------------------------
 redefine attr f is empty-yielding means
   for x st x in dom f holds f.x is empty;
 compatibility
  proof
  ...
  end;
-------------------------------

Michael Nedzelsky