[mizar] Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi All,

The article tex_4.miz contains the following fragment (lines 2488 - 2493):

-------------------------------
registration let Y be non empty TopStruct,
  A be non empty Subset of Y;
 canceled;
 cluster Sspace(A) -> non empty;
 coherence;
end;
-------------------------------

It seems the following rule must be added to the grammar:

Canceled-Registration =
	"canceled" [ Numeral ] ";" .

and the rule for Cluster-Registration must be changed:

From:

Cluster-Registration =
	Existential-Registration | Conditional-Registration | 
Functorial-Registration .

To:

Cluster-Registration =
	Existential-Registration | Conditional-Registration | Functorial-Registration
	| Canceled-Registration .

Michael Nedzelsky