*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Sat, 24 Nov 2012 10:04:03 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1211231619050.8370@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> <50AEBADA.406@rsise.anu.edu.au> <alpine.LNX.2.00.1211231619050.8370@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

Makarius, On 11/24/2012 02:25 AM, Makarius wrote:

On Fri, 23 Nov 2012, Jeremy Dawson wrote:Obviously, nothing that has been implemented in Standard ML couldn't be packaged in a way to make it convenient for users to use by calling Standard ML functions. The fact that the developers have not done so doesn't add to the merits of Isar (the language and its grammar).The Isar proof method called "tactic" actually presents the ML name space to the user in a way that you can write nostalgic tactic expressions right into your Isar proofs. E.g. like this: lemma "A & B --> B & A" apply (tactic "rtac impI 1") apply (tactic "etac conjE 1") apply (tactic "rtac conjI 1") apply (tactic "ALLGOALS atac") done

Giving a name to a tactics-expression, I would want the ML code that does something like val meth4 = EVERY [(TRY (REPEAT1 meth1)), meth2, meth3 ] ; made accessible.

So it is basically the same like in 1993, just with some extra boiler plate. There is no practical point to use the above in reality, though.

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

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

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

- Previous by Date: Re: [isabelle] quotient_of: missing lemma
- Next by Date: Re: [isabelle] Context Free Language
- 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