# [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.*