*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 23 Nov 2012 10:52:58 +1100*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1211221339220.19500@macbroy21.informatik.tu-muenchen.de>*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> <50AC4179.7070101@rsise.anu.edu.au> <49EAB30D-6FC1-4B09-A576-12094F24F98A@cam.ac.uk> <50AD562E.5090103@rsise.anu.edu.au> <alpine.LNX.2.00.1211221339220.19500@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.13) Gecko/20101209 Fedora/3.1.7-0.35.b3pre.fc14 Thunderbird/3.1.7

On 11/22/2012 11:42 PM, Makarius wrote:

On Thu, 22 Nov 2012, Jeremy Dawson wrote:Given that in HOL (as in Isabelle, both pre and post Isar) one can always use proof procedures coded by someone else, this seems to sum up to saying that Isabelle/Isar is like HOL, minus the capacity to code one's own proof procedures, plus -- what ??From where did you get the "minus"? Certainly not from this thread, where I've pointed to the method_setup command of Isabelle/Isar already. It is document in the "isar-ref" manual, as all other Isar commands. The "implementation" manual has further documentation about what proof methods are, compared to bare-bones tactics (which are also documented there).

Makarius,

The "plus" is much more than be discussed on such a mail thread. It also depends on the imagination of users, what they make out of the vast formal environment that Isabelle gives you today (as of current Isabelle2012).

Jeremy

Makarius

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

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

**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:*Makarius

- Previous by Date: Re: [isabelle] Length of Proofs
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- 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