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
Isabelle/804dfdc82835:
* 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
or:
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.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev