Hi Josef,
At the end of http://www.mizar.org/language/syntax.html there is a string:
Done with grammar2thtml.xsl
It seems that the syntax.html was built from some XML-file for Mizar grammar.
Is it XML-file still available anywhere?
May be this question must be addressed to Grzegorz Bancerek, though I hope he
use this mail list too. :)
looks like a bug, the grammar version at
http://mizar.org/language/pages/predicate-definition.html#predicate-definit
ion with Correctness-Conditions instead of [ "correctness" Justification ";"
] seems more correct.
The version was last modified: June 26, 2000 and seems more correct than
both http://www.mizar.org/language/syntax.html (February 10, 2005)
and syntax.txt (May 5, 2006). Entropy process? :)
Why I am interested in it:
I have written a converter from syntax.txt to XML-file in order to get
better understanding Mizar grammar.
there is no automated (e.g. bison-like) connection between them and the
Mizar parser.
I thougt about using Elkhound (GLR parsing)
http://www.cs.berkeley.edu/~smcpeak/elkhound
or implementation GLR in OCaml
but for now my simple toy parser (in Ocaml) is coded by hand.
Michael Nedzelsky