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