Re: [isabelle] Length of Proofs


My understanding has been that you - or someone - introduced new features in Isabelle which were accessible only from Isar, not from the Standard ML interface.

In my book this discourages the use of Standard ML, and also provides an explanation for it having "come out of use", regardless of its relative merits as a user interface language.

I don't understand your reference to SSReflect. How would that help me do Isabelle proofs?


On 11/17/2012 08:27 AM, Makarius wrote:
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 MHonArc.