Re: [isabelle] Ways to use expression shorthands in proof?
Le Sat, 04 Aug 2012 16:24:18 +0200, Gottfried Barrow
<gottfried.barrow at gmx.com> a écrit:
For an interesting discussion of an explicit proof example using
introduction and elimination rules, scroll down to Wenzel's PhD thesis
on the page below, and have a look at pages 77 to 92 where he takes a
simple example and starts with a very abbreviated form and keeps
expanding it into more explicit forms.
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 like
with my discovery of Isabelle: as I go, I understand it's intentionally
designed to author concise and readable proof, and to balance both
(conciseness and verbosity) as you see fits.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and