[isabelle-dev] NEWS: structured Isar goal statements (update)

Makarius makarius at sketis.net
Sat Jun 27 00:38:52 CEST 2015

On Wed, 24 Jun 2015, Makarius wrote:

> The keyword 'when' may be used instead of 'if', to indicate 'presume'
> instead of 'assume' above.
> This refers to Isabelle/51a6997b1384.
> The 'presume' element is rarely used, and the 'when' eigen-context is mainly 
> an exercise in orthogonality of the language. There might be useful 
> applications nonetheless, e.g. see the examples about "suffices-to-show" in 
> ~~/src/HOL/Isar_Examples/Structured_Statements.thy

Now that 'presume' semantics has a separate syntax, the normal ==> is free 
to be re-interpreted.  So here is another breaking NEWS entry for 

* The meaning of 'show' with Pure rule statements has changed: premises
are treated in the sense of 'assume', instead of 'presume'. This means,
a goal like "⋀x. A x ⟹ B x ⟹ C x" can be solved completely as follows:

   show "⋀x. A x ⟹ B x ⟹ C x"


   show "C x" if "A x" "B x" for x

Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

   show "C x" when "A x" "B x" for x

This means the common beginner-mistake to use Pure rule statements for 
show no longer leads to bad surprises.  As a consequence, there might be 
more ugly proofs emerging than necessary, but better than no proof at all 
in the first attempt.


More information about the isabelle-dev mailing list