--- a/NEWS Mon Jun 22 19:22:48 2015 +0200
+++ b/NEWS Mon Jun 22 20:36:33 2015 +0200
@@ -20,7 +20,8 @@
* 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"
@@ -38,6 +39,9 @@
}
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).