[isabelle] Raw proof blocks



In section 2.6 ("Raw proof blocks") of "A Tutorial Introduction to Structured Isar Proofs," there appears the following sentence at the top of page 13: "Note that the conclusion of a raw proof block is stated with 'have' rather than 'show' because it is not the conclusion of some pending goal but some independent claim." Yet in theory Fields, in the section (14.1) on division rings, there is a proof of the right-inverse-eq lemma that contains a raw proof block (at least I assume it is a raw proof block -- it is contained in curly brackets) that ends in 'show.' Is this just a bug, or is it a version of raw proof blocks that isn't described in the Tutorial Introduction?
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




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