*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Ways to use expression shorthands in proof?*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Sun, 05 Aug 2012 02:39:45 +0200*Organization*: Ada @ Home*References*: <op.wiimlklrule2fv@douda-yannick> <501D3092.10807@gmx.com> <op.wii32loqule2fv@douda-yannick> <501D75CA.20607@gmx.com>*User-agent*: Opera Mail/12.01 (Linux)

On 8/4/2012 1:24 PM, Yannick Duchêne (Hibou57) wrote:Currently on the page 77 you mentioned, looking at “is” and “concl is”.Looks even shorter and straighter than using “let”. That's what I likewith my discovery of Isabelle: as I go, I understand it's intentionallydesigned to author concise and readable proof, and to balance both(conciseness and verbosity) as you see fits.The page 77 you're talking about is the absolute page number, whichwould be the printed page number of 63.The example I'm talking about is sections 4.2.3 and 4.2.4, printed pagenumbers 77 to 92.It goes to show that there are lots more examples and explanations inthat document on Isar. For each keyword described in Wenzel's document,if you look the keyword up in isar-ref.pdf, then you learn even more.Regards, GB

Thanks for your tips, to both of you -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Attachment:
Isa_Test.thy**

**Attachment:
Isa_Test.pdf**

**References**:**[isabelle] Ways to use expression shorthands in proof?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Ways to use expression shorthands in proof?***From:*Gottfried Barrow

**Re: [isabelle] Ways to use expression shorthands in proof?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Ways to use expression shorthands in proof?***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Syntax issue: lost between HOL and Isar
- Next by Date: Re: [isabelle] Isabelle 2012 on Win7
- Previous by Thread: Re: [isabelle] Ways to use expression shorthands in proof?
- Next by Thread: [isabelle] Isabelle 2012 on Win7
- Cl-isabelle-users August 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