NEWS

 * Term abbreviations via 'is' patterns also work for schematic
 statements: result is abstracted over unknowns.
 
 * Local goals ('have', 'show', 'hence', 'thus') allow structured
 statements like fixes/assumes/shows in theorem specifications, but the
-notation is postfix with keywords 'if' and 'for'. For example:
+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>

     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.
 
 * New command 'supply' supports fact definitions during goal refinement
 ('apply' scripts).
 
 * New command 'consider' states rules for generalized elimination and