*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Length of Proofs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 26 Nov 2012 22:43:19 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1211261119150.14277@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> <50B000E3.4010105@rsise.anu.edu.au> <alpine.LNX.2.00.1211261119150.14277@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,

Cheers, Jeremy On 11/26/2012 09:27 PM, Makarius wrote:

On Sat, 24 Nov 2012, Jeremy Dawson wrote: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") doneAnother misunderstanding, I'm afraid. The above is about using ML from within Isar. I'm referring to the theoretical possibility of calling features of the Isar structure/framework from within ML. Such as, for example, as discussed in Feb 2010 in the thread called I think this email thread is getting too long - my first post was of stuff that I asserted (and still do) that you can't imagine how to do it sensibly other than in Standard ML.The thread is indeed getting long and tedious, and it is unclear if it ever ends. When I say "ML" or "Isabelle/ML", it practically always means the ML that is embedded into Isar. This is what you use for professional applications these days. There is also a raw ML bootstrap environment to get the Isabelle/Pure implementation to the point where it can run the Isar toplevel with this embedded ML. In the 1990-ies, the user would continue with that raw ML toplevel to do proofs, but hardly anybody on the mailing list would remember that today. Insisting to work with the raw ML toplevel is like traveling on a train like this: http://gehcrew.blogspot.fr/2010_03_01_archive.html This technique works for a tramway to some extent, but not on the high-speed train that Isabelle has become in recent years, where you better sit comfortably inside. And to get on such a train you merely purchase a ticket, you don't come with its technical manuals and take the engine apart while it is moving. 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

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

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

- Previous by Date: Re: [isabelle] Naming cases in the induction scheme of a function
- Next by Date: Re: [isabelle] syntax annotations
- Previous by Thread: Re: [isabelle] Length of Proofs
- Next by Thread: Re: [isabelle] Print proof of theorem
- 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