--- 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