--- a/NEWS Fri Jun 26 18:54:23 2015 +0200
+++ b/NEWS Sat Jun 27 00:10:24 2015 +0200
@@ -42,6 +42,20 @@
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
+* 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 "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
+
+ show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> 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
+
* New command 'supply' supports fact definitions during goal refinement
('apply' scripts).