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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and