Mizar syntax

-- GrzegorzBancerek - 12 Dec 2007

Redefinition-Block cannot repeat (it is intention, not practice(?)). In Identify-Registration, the intention is to use Loci after "when". In Predicate-Definition [ "correctness" ... ] changed to Correctness-Conditions.

-- MichaelNedzelsky - 13 Apr 2007

Thanks to Adam Grabowski, the Mizar grammar has been corrected ("identify" rule was added).

Also the name of xml grammar file has been changed from mizar.xml to syntax.xml in order to avoid confusion with the Mizar.xml file, which is already in the Mizar distribution.

-- MichaelNedzelsky - 27 Oct 2006

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

-- MichaelNedzelsky - 26 Oct 2006

The following rules were changed in order to support predefined mode "set", functor brackets "{", "[", "}", "]" and predicate "=":

Mode-Symbol, Left-Functor-Bracket, Right-Functor-Bracket, Predicate-Symbol.

-- MichaelNedzelsky - 23 Oct 2006

The following rules were changed:

Definitional-Block, Attribute-Definition, Cluster-Registration, Functorial-Registration.

The nonterminal Canceled-Registration was added to the grammar.

-- GrzegorzBancerek - 17 Oct 2006

Initial posting of xml files.

• syntax.xml: Mizar syntax according to grammar.dtd

• grammar.dtd: DTD for grammars

• grammar2thtml.xsl: XML grammar to HTML with tables transformation stylesheet

• grammar2ntxt.xsl: XML grammar to plain text transformation stylesheet