Re: [isabelle] Isabelle-Isar grammar?



On Thu, 8 Mar 2012, Siddhartha Gadgil wrote:

       I was wondering if there was a document giving a grammar for
Isabelle-Isar similar to the Mizar one at
http://mizar.uwb.edu.pl/version/current/doc/syntax.txt? The
Isabelle/Isar Quick reference is very elegant : what I was looking for
was the same at lower levels as well

The same manual contains more detailed syntax diagrams for each individual command.

e.g. the internal type system defining theorem etc.

What exactly do you mean by this? The section on "The Isabelle/Isar Framework" in the same manual gives some hints how Isar proof texts are interpreted wrt. Isabelle/Pure inferences. Maybe that is getting closer to what you are looking for.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.