*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Tue, 20 Nov 2012 10:08:13 +1100*Cc*: Makarius <makarius at sketis.net>, Jens Doll <jd at cococo.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <E20FDEC0-25AE-4C90-B51B-0510141A586B@cam.ac.uk>*References*: <50921697.9090307@cococo.de> <50921DCB.6050502@rsise.anu.edu.au> <alpine.LNX.2.00.1211162218270.24652@macbroy20.informatik.tu-muenchen.de> <50A728D8.2070105@rsise.anu.edu.au> <E20FDEC0-25AE-4C90-B51B-0510141A586B@cam.ac.uk>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

Larry,

Jeremy Lawrence Paulson wrote:

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. Larry On 17 Nov 2012, at 06:04, Jeremy Dawson <jeremy at rsise.anu.edu.au> 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.

**Follow-Ups**:**Re: [isabelle] Length of Proofs***From:*Makarius

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

**References**:**[isabelle] Length of Proofs***From:*Jens Doll

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Makarius

**Re: [isabelle] Length of Proofs***From:*Jeremy Dawson

**Re: [isabelle] Length of Proofs***From:*Lawrence Paulson

- Previous by Date: [isabelle] syntax annotations
- Next by Date: Re: [isabelle] syntax annotations
- Previous by Thread: Re: [isabelle] Length of Proofs
- Next by Thread: Re: [isabelle] Length of Proofs
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list