# HG changeset patch
# User nipkow
# Date 908552172 -7200
# Node ID 1a6c9c6a3f8ed8de896575d8900a59fdffaf360a
# Parent  f8389824189b83e4529eebc4a9097f34b70a7196
  2. The simplifier now knows a little bit about nat-arithmetic.

diff -r f8389824189b -r 1a6c9c6a3f8e NEWS
--- a/NEWS	Fri Oct 16 17:33:43 1998 +0200
+++ b/NEWS	Fri Oct 16 17:36:12 1998 +0200
@@ -31,13 +31,15 @@
 
 *** Proof tools ***
 
-* Simplifier: 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.
+* Simplifier:
+  1. 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.
+  2. The simplifier now knows a little bit about nat-arithmetic.
 
 * Classical reasoner: wrapper mechanism for the classical reasoner now
 allows for selected deletion of wrappers, by introduction of names for