--- a/NEWS Tue Jul 14 13:31:55 1998 +0200
+++ b/NEWS Tue Jul 14 13:33:12 1998 +0200
@@ -149,11 +149,17 @@
* directory HOL/UNITY: Chandy and Misra's UNITY formalism;
+* calling (stac rew i) now fails if "rew" has no effect on the goal
+ [previously, this check worked only if the rewrite rule was unconditional]
+
*** ZF ***
* in let x=t in u(x), neither t nor u(x) has to be an FOL term.
+* calling (stac rew i) now fails if "rew" has no effect on the goal
+ [previously, this check worked only if the rewrite rule was unconditional]
+
*** Internal programming interfaces ***
@@ -170,6 +176,8 @@
* Pure: several new basic modules made available for general use, see
also src/Pure/README;
+* new tactical CHANGED_GOAL for checking that a tactic modifies a subgoal
+
New in Isabelle98 (January 1998)