*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Length of Proofs*From*: Makarius <makarius at sketis.net>*Date*: Mon, 26 Nov 2012 11:27:37 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50B000E3.4010105@rsise.anu.edu.au>*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>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 fromwithin Isar. I'm referring to the theoretical possibility of callingfeatures of the Isar structure/framework from within ML. Such as, forexample, as discussed in Feb 2010 in the thread calledI think this email thread is getting too long - my first post was ofstuff that I asserted (and still do) that you can't imagine how to do itsensibly other than in Standard ML.

Makarius

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

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

- Previous by Date: [isabelle] [symmetric]-attribute changes variable names
- Next by Date: Re: [isabelle] Naming cases in the induction scheme of a function
- 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