NEWS
changeset 23495 e4dd6beeafab
parent 23481 93dca7620d0d
child 23509 14a2f87ccc73
     1.1 --- a/NEWS	Mon Jun 25 12:16:27 2007 +0200
     1.2 +++ b/NEWS	Mon Jun 25 14:49:32 2007 +0200
     1.3 @@ -1681,6 +1681,21 @@
     1.4    mult_neg           now named mult_neg_neg
     1.5    mult_neg_le        now named mult_nonpos_nonpos
     1.6  
     1.7 +* The following lemmas in Ring_and_Field have been added to the simplifier:
     1.8 +     
     1.9 +     zero_le_square
    1.10 +     not_square_less_zero 
    1.11 +
    1.12 +  The following lemmas have been deleted from Real/RealPow:
    1.13 +  
    1.14 +     realpow_zero_zero
    1.15 +     realpow_two
    1.16 +     realpow_less
    1.17 +     zero_le_power
    1.18 +     realpow_two_le
    1.19 +     abs_realpow_two
    1.20 +     realpow_two_abs     
    1.21 +
    1.22  * Theory Parity: added rules for simplifying exponents.
    1.23  
    1.24  * Theory List: