Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Eisbach User Manual (was: Isabelle2015-RC5 ava...

Email Gateway (Aug 22 2022 at 09:52):

From: Lars Noschinski <noschinl@in.tum.de>
I read the document and got a few remarks:

• Page 2, paragraph 2 there is a "." missing between "syntax" and "These".
• Page 3, paragraph 1 of 1.3.1: undefined reference
• Page 9, paragraph 1 of 2.1: undefined reference
• Page 9, second lemma: "conclusion" probably ought to be bold
• Page 10, first methode: "premises in" probably ought to be bold

• Page 13, first lemma in 2.2: I read asms as "A ==> B A ==> D" instead
  as "A ==> B" "A ==> D". Maybe more space?

• Page 16, first lemma in 2.4.2: "in" probably ought to be bold -- there
  a further instances of this formatting in the document

• Page 20, paragraph 1: "cast distinction" -> "case distinction"

• Page 20, paragraph 2: "fist matching" -> "first matching"

  -- Lars

Last updated: Apr 19 2024 at 08:19 UTC