Re: [isabelle] Length of Proofs

As I see it, there are advantages to both interfaces. And everything is accessible from ML simply because it is the implementation language, although of course this access may not be very convenient. I think it's generally accepted these days that the ML level really is more appropriate for development than for ordinary reasoning. It isn't realistic to support both Isar and the ML level as the day-to-day user interface; even with unlimited resources, such duplication wouldn't be very elegant.

Isabelle has undergone very rapid change over the years, and this has meant leaving a lot of old practices behind. I know that it has caused users difficulties in the past, and it's unfortunate, but maintaining upwards compatibility is also very difficult. As one of the earliest Isabelle users, you naturally feel this much more than others do.


On 17 Nov 2012, at 06:04, Jeremy Dawson <jeremy at> wrote:

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.