diff -r 1430360d9782 -r 12290bdce807 NEWS
--- a/NEWS	Tue Oct 01 14:45:28 2002 +0200
+++ b/NEWS	Tue Oct 01 15:03:28 2002 +0200
@@ -6,6 +6,38 @@
 
 *** General ***
 
+* Provers/simplifier:
+
+  - Completely reimplemented Asm_full_simp_tac:
+    Assumptions are now subject to complete mutual simplification,
+    not just from left to right. The simplifier now preserves
+    the order of assumptions.
+
+    Potential INCOMPATIBILITY:
+
+    -- Asm_full_simp_tac sometimes diverges where the old version did
+       not, e.g. invoking Asm_full_simp_tac on the goal
+
+        [| P (f x); y = x; f x = f y |] ==> Q
+
+      now gives rise to the infinite reduction sequence
+
+        P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ...
+
+      Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead
+      often solves this kind of problem.
+
+    -- Tactics combining classical reasoner and simplification (such
+       as auto) are also affected by this change, because many of them
+       rely on Asm_full_simp_tac. They may sometimes diverge as well
+       or yield a different numbers of subgoals. Try to use e.g. force,
+       fastsimp, or safe instead of auto in case of problems. Sometimes
+       subsequent calls to the classical reasoner will fail because a
+       preceeding call to the simplifier too eagerly simplified the
+       goal, e.g. deleted redundant premises.
+
+  - The simplifier trace now shows the names of the applied rewrite rules
+
 * Pure: locale specifications now produce predicate definitions
 according to the body of text (covering assumptions modulo local
 definitions); predicate "loc_axioms" covers newly introduced text,
@@ -72,8 +104,6 @@
 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands
 are distributed over a sum of terms;
 
-* the simplifier trace now shows the names of the applied rewrite rules
-
 * induct over a !!-quantified statement (say !!x1..xn):
   each "case" automatically performs "fix x1 .. xn" with exactly those names.