[mizar] Changes in the Mizar grammar file.

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi all,

The optional label has been added at the beginning of the Iterative-Equality 
production rule.

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

From:
Iterative-Equality =
	Term-Expression "=" Term-Expression Simple-Justification ".=" Term-Expression 
Simple-Justification { ".=" Term-Expression Simple-Justification } ";" .

To:
Iterative-Equality = [ Label-Identifier ":" ]
	Term-Expression "=" Term-Expression Simple-Justification ".=" Term-Expression 
Simple-Justification { ".=" Term-Expression Simple-Justification } ";" .


Justification: the following fragment from MML.
  xboole_1.miz: lines 995 - 1003.
-------------------------------
theorem :: AMI_1'12:
     X misses Y \ Z implies Y misses X \ Z
proof
A1: X /\ (Y \ Z) = Y /\ X \ Z by Th49
     .= Y /\ (X \ Z) by Th49;
    (X misses Y \ Z iff X /\ (Y \ Z) = {}) &
 (Y misses X \ Z iff Y /\ (X \ Z) = {}) by XBOOLE_0:def 7;
 hence thesis by A1;
end;
-----------------------------------------------

Regards,
  Michael Nedzelsky