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

On Fri, 23 Nov 2012, Jeremy Dawson wrote:

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).There is an ambiguity here between Isar (the language and its grammar)and Isar (the design/structure, ie, methods, facts, etc).

Obviously, nothing that has been implemented in Standard ML couldn't bepackaged in a way to make it convenient for users to use by callingStandard ML functions. The fact that the developers have not done sodoesn't add to the merits of Isar (the language and its grammar).

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

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

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