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 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.


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