Re: [isabelle] Raw proof blocks

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

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

I did try to look up "raw proof blocks" in the isar-ref manual ("The Isabelle Isar Reference Manual," December 2013) but "raw proof blocks" is not in the Index of that manual (either under "raw" or under "proof" or under "blocks"). Am I misunderstanding how to use that manual?

It is a reference manual, which means you don't read it from start to end in one go, but look occasionally if there are relevant bits and pieces. Taking all that information together, some mental picture of what Isar actually is should emerge. You should skim through the table of contents to get an idea of the different areas that are covered.

Chapter 6 is about proofs. Section 6.1 about proof structure. Blocks are described in 6.1.2 --- some abstract text about that concept. At least it says something about 'next' and also mentions 'show' in a way that indicates that it can be used here.

BTW, the current version of Isabelle is from August 2014 and the manual has the same date. As a habit you should follow the normal Isabelle release cycle, unless there are special reasons to stick to an older version.



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