Re: [isabelle] Length of Proofs
On Thu, 22 Nov 2012, Lawrence Paulson wrote:
You still have the capacity to code your own proof procedures; ML is
just one level down. And you get a much more readable proof language.
The situation is a bit more general than this, and it is hard to arrange
Isar vs. ML in "levels" in particular. Both are intertwined, cf. my
explanation of Isabelle/Isar and Isabelle/ML as as the Yin and Yang of
In general Isar vs. its embedded languages works like this:
* Isar is the main framework of Isabelle to integrate many
* The Isar languages for specifications (e.g. 'theorem', 'definition',
'function') and proofs (e.g. 'fix', 'assume', 'show' ...) are the
primary applications of the Isar framework.
* The logical language (Pure types/terms/propositions with specific HOL
notation) is another important embedded language, cf. the quotes that
have been around this language even in the ancient ML-only times of
Isabelle in the 1990-ies.
* ML is embedded into Isar in a similar manner, but at the same
time it is the implementation language of Isar. Moreover, ML quoted
inside Isar can antiquote logic/Isar expressions. So the image for
that is http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg
In everyday life you don't use the ML inside Isar a lot, but you can
whenever you need to. It is more convenient than the ancient ML toplevel
ever was. In Isabelle/jEdit you also have substantial IDE integration for
this ML inside Isar.
This archive was generated by a fusion of
Pipermail (Mailman edition) and