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

[Makarius]

* 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 local assumptions are bound to the name "that". The result is
exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:

   {
     fix x :: 'a and y :: 'a
     assume that: "A x" "B y"
     have "C x y" <proof>
   }
   note result = this

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


 	Makarius