# Re: [isabelle] Raw proof blocks

On Sun, 19 Oct 2014, W. Douglas Maurer wrote:

`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?
`

`Whenever the meaningless word "bug" comes up, there is a high chance that
``it is a misunderstanding of the user.
`

`A tutorial is not necessarily complete and exhaustive, in contrast to a
``reference manual. Isabelle has lots of manuals with different approaches
``to explain things. Ultimately the authoritative source for Isar is the
``isar-ref manual (and of course the implementation). So if the system
``accepts some proof text, it is probably right.
`

`According to the inner workings of Isar, it is of course possible to use
``raw proof blocks { } together with fix-assume-show of regular proof
``bodies. It is not used very often, but it definitely has its uses. It
``allows to manage local contexts with further depth, instead of the
``immediate default context of the original goal statement.
`

`You can also use the block separator 'next' within { } even though some
``explanations sometimes tell a different story.
`
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org
----------------------------------------------------------------------------

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