diff -r 6a699d5cdef4 -r 3ca4da83012c NEWS
--- a/NEWS	Wed Aug 12 17:40:18 1998 +0200
+++ b/NEWS	Thu Aug 13 17:28:19 1998 +0200
@@ -223,7 +223,7 @@
 
 * 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]
-
+  Now rew can involve either definitions or equalities (either == or =).
 
 *** ZF ***
 
@@ -242,6 +242,7 @@
 
 * 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]
+  Now rew can involve either definitions or equalities (either == or =).
 
 * case_tac provided for compatibility with HOL
     (like the old excluded_middle_tac, but with subgoals swapped)