# HG changeset patch
# User obua
# Date 1182775772 -7200
# Node ID e4dd6beeafabc0f2f161a0bb612dba0d243feaa4
# Parent  f985f9239e0d79c3258cb9840f7f916ea6cb7a60
commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy

diff -r f985f9239e0d -r e4dd6beeafab NEWS
--- a/NEWS	Mon Jun 25 12:16:27 2007 +0200
+++ b/NEWS	Mon Jun 25 14:49:32 2007 +0200
@@ -1681,6 +1681,21 @@
   mult_neg           now named mult_neg_neg
   mult_neg_le        now named mult_nonpos_nonpos
 
+* The following lemmas in Ring_and_Field have been added to the simplifier:
+     
+     zero_le_square
+     not_square_less_zero 
+
+  The following lemmas have been deleted from Real/RealPow:
+  
+     realpow_zero_zero
+     realpow_two
+     realpow_less
+     zero_le_power
+     realpow_two_le
+     abs_realpow_two
+     realpow_two_abs     
+
 * Theory Parity: added rules for simplifying exponents.
 
 * Theory List: