Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle-Isar grammar?

Email Gateway (Aug 18 2022 at 19:16):

From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
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 (e.g. the internal type system
defining theorem etc.)
thanks,
Siddhartha

Email Gateway (Aug 18 2022 at 19:18):

From: Makarius <makarius@sketis.net>
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

Last updated: May 01 2024 at 20:18 UTC