commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
authorobua
Mon Jun 25 14:49:32 2007 +0200 (2007-06-25)
changeset 23495e4dd6beeafab
parent 23494 f985f9239e0d
child 23496 84e9216a6d0e
commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
NEWS
     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: