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
* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' (or 'when') and 'for'. For
example:
have result: C x y
if A x and B y
for x :: 'a and y :: 'a
proof
The
