*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 21 Nov 2012 13:50:33 +1100*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <98A92B35-BD03-4E31-B0E5-BBD552920CF6@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> <50AABBDD.70700@rsise.anu.edu.au> <98A92B35-BD03-4E31-B0E5-BBD552920CF6@cam.ac.uk>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

Larry,

Cheers, Jeremy Lawrence Paulson wrote:

I think it's a great pity that you are using such an elderly version of Isabelle. If you have a lot of legacy code that simply can't be ported, or an application where it works really well, okay. But for general proofs, there is simply no comparison between the Isabelle of today and one that is seven years old. Sledgehammer, counterexample finding, a very powerful function definition package, lots and lots of AFP theories… You shouldn't forego all of those. Larry

**Follow-Ups**:**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

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

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

- Previous by Date: Re: [isabelle] Documentation of ML sources
- Next by Date: Re: [isabelle] Feature wish: Minimal simp/auto invocations
- 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