# HG changeset patch
# User paulson
# Date 900415992 -7200
# Node ID c56aa8b59dc0da1c2349587a0e4eded3d538560e
# Parent  495a4f9af897070ed58e7adb06931dd77601e058
new stac

diff -r 495a4f9af897 -r c56aa8b59dc0 NEWS
--- 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)