*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*: Sat, 04 Aug 2012 20:24:11 +0200*Organization*: Ada @ Home*References*: <op.wiimlklrule2fv@douda-yannick> <501D3092.10807@gmx.com>*User-agent*: Opera Mail/12.01 (Linux)

For an interesting discussion of an explicit proof example usingintroduction and elimination rules, scroll down to Wenzel's PhD thesison the page below, and have a look at pages 77 to 92 where he takes asimple example and starts with a very abbreviated form and keepsexpanding it into more explicit forms.http://www4.in.tum.de/~wenzelm/papers/ <http://www4.in.tum.de/%7Ewenzelm/papers/>

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

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

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

- Previous by Date: Re: [isabelle] Isabelle 2012 on Win7
- Next by Date: Re: [isabelle] Ways to add a checking layer for Theories?
- Previous by Thread: Re: [isabelle] Ways to use expression shorthands in proof?
- Next by Thread: Re: [isabelle] Ways to use expression shorthands in proof?
- 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