diff -r e1888c0d3b36 -r b1d916e8a853 NEWS
--- a/NEWS	Wed Mar 11 09:40:32 1998 +0100
+++ b/NEWS	Wed Mar 11 09:50:31 1998 +0100
@@ -7,7 +7,8 @@
 
 * Rewrite rules for case distinctions can now be added permanently to the
   default simpset using Addsplits just like Addsimps. They can be removed via
-  Delsplits just like Delsimps. For applications see HOL below.
+  Delsplits just like Delsimps. Lower-case versions are also available.
+  For applications see HOL below.
 
 * Changed wrapper mechanism for the classical reasoner now allows for selected
   deletion of wrappers, by introduction of names for wrapper functionals.
@@ -24,7 +25,9 @@
 
 * HOL/Arithmetic: removed 'pred' (predecessor) function;
 
-* The rule expand_if is now part of the default simpset. This means that
+* Simplifier:
+
+ -The rule expand_if is now part of the default simpset. This means that
   the simplifier will eliminate all ocurrences of if-then-else in the
   conclusion of a goal. To prevent this, you can either remove expand_if
   completely from the default simpset by `Delsplits [expand_if]' or
@@ -34,6 +37,14 @@
   simpset: every datatype generates a suitable rule `split_t_case' (where t
   is the name of the datatype).
 
+ -Asm_full_simp_tac is now more aggressive:
+  1. It will sometimes reorient premises if that increases their power to
+     simplify.
+  2. It does no longer proceed strictly from left to right but may also
+     rotate premises to achieve further simplification.
+  For compatibility reasons there is now Asm_lr_simp_tac which is like the
+  old Asm_full_simp_tac in that it does not rotate premises.
+
 * new theory Vimage (inverse image of a function, syntax f-``B);
 
 * many new identities for unions, intersections, etc.;