Re: [isabelle] Ways to use expression shorthands in proof?

Le Sat, 04 Aug 2012 16:24:18 +0200, Gottfried Barrow <gottfried.barrow at> 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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.