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



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.

Regards,
GB






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