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

Le Sat, 04 Aug 2012 21:19:38 +0200, Gottfried Barrow <gottfried.barrow at> a écrit:

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

The page 77 you're talking about is the absolute page number, which would be the printed page number of 63.

The example I'm talking about is sections 4.2.3 and 4.2.4, printed page numbers 77 to 92.

It goes to show that there are lots more examples and explanations in that 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.


I finally go with both Brian's suggestion to use “let” and Markus's thesis suggestion to use “"…" (is "…")”. I ended to the test files attached to that message. Please note that's nothing exiting, just intended to beginners like me, and to be opened to comments (comments are easier on simple things). It's based on something from a function tutorial in Isabelle's documentation directory. I'm not so much happy with the PDF rendering, but I don't know enough about (La)Tex, that may be the reason why (I also wonder why the document weight more than expected, but that's another story).

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
Description: Binary data

Attachment: Isa_Test.pdf
Description: Adobe PDF document

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