2. The simplifier now knows a little bit about nat-arithmetic.
authornipkow
Fri Oct 16 17:36:12 1998 +0200 (1998-10-16)
changeset 56571a6c9c6a3f8e
parent 5656 f8389824189b
child 5658 082debccf486
2. The simplifier now knows a little bit about nat-arithmetic.
NEWS
     1.1 --- a/NEWS	Fri Oct 16 17:33:43 1998 +0200
     1.2 +++ b/NEWS	Fri Oct 16 17:36:12 1998 +0200
     1.3 @@ -31,13 +31,15 @@
     1.4  
     1.5  *** Proof tools ***
     1.6  
     1.7 -* Simplifier: Asm_full_simp_tac is now more aggressive.
     1.8 -  1. It will sometimes reorient premises if that increases their power to
     1.9 -     simplify.
    1.10 -  2. It does no longer proceed strictly from left to right but may also
    1.11 -     rotate premises to achieve further simplification.
    1.12 -  For compatibility reasons there is now Asm_lr_simp_tac which is like the
    1.13 -  old Asm_full_simp_tac in that it does not rotate premises.
    1.14 +* Simplifier:
    1.15 +  1. Asm_full_simp_tac is now more aggressive.
    1.16 +     1. It will sometimes reorient premises if that increases their power to
    1.17 +        simplify.
    1.18 +     2. It does no longer proceed strictly from left to right but may also
    1.19 +        rotate premises to achieve further simplification.
    1.20 +     For compatibility reasons there is now Asm_lr_simp_tac which is like the
    1.21 +     old Asm_full_simp_tac in that it does not rotate premises.
    1.22 +  2. The simplifier now knows a little bit about nat-arithmetic.
    1.23  
    1.24  * Classical reasoner: wrapper mechanism for the classical reasoner now
    1.25  allows for selected deletion of wrappers, by introduction of names for