Re: [isabelle] Length of Proofs
On Thu, 1 Nov 2012, Jeremy Dawson wrote:
In such a case it is advantageous not to have to write them all down
repeatedly, but to reuse them. The Standard ML interface to Isabelle is
ideally suited to this purpose. Unfortunately its use has become
actively discouraged in recent years.
As far as I am concerned, I never discouraged the use of Isabelle/ML, it
merely came out of use as proof scripting languages, because there are
better ways these days. Christian Sternagel has already hinted at the
fine art to combine structured Isar proof elements, and an assorted
collection with proof tools.
If you still want to have hard-core quick script hacking, the community
for that is centered around SSReflect, which is continuing traditions of
APL for proof recording. The scripts then come out very tight and terse,
by experts for experts.
I am still keen to seen such a quick-hacking approach turned into proper
use for an advanced Prover IDE: instead of recording the gesticulation of
the author in the script, it would produce a nice structured, readable,
maintainable proof document.
This archive was generated by a fusion of
Pipermail (Mailman edition) and