# HG changeset patch
# User huffman
# Date 1273604719 25200
# Node ID 49156805321cc5835977672fc5c115444d384d25
# Parent  7902dc7ea11d56ba74665c8392a6d03f5a7c9185
removed lemma real_sq_order; use power2_le_imp_le instead

diff -r 7902dc7ea11d -r 49156805321c NEWS
--- a/NEWS	Tue May 11 11:58:34 2010 -0700
+++ b/NEWS	Tue May 11 12:05:19 2010 -0700
@@ -143,7 +143,11 @@
 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
 no longer shadowed.  INCOMPATIBILITY.
 
-* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
+* Dropped theorem duplicate comp_arith; use semiring_norm instead.
+INCOMPATIBILITY.
+
+* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
+INCOMPATIBILITY.
 
 * Theory 'Finite_Set': various folding_* locales facilitate the application
 of the various fold combinators on finite sets.
diff -r 7902dc7ea11d -r 49156805321c src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue May 11 11:58:34 2010 -0700
+++ b/src/HOL/RealPow.thy	Tue May 11 12:05:19 2010 -0700
@@ -88,17 +88,4 @@
 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
 by (auto simp add: power2_eq_square)
 
-(* The following theorem is by Benjamin Porter *)
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma real_sq_order:
-  fixes x :: "'a::linordered_semidom"
-  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
-  shows "x \<le> y"
-proof -
-  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
-    by (simp only: numeral_2_eq_2)
-  thus "x \<le> y" using ygt0
-    by (rule power_le_imp_le_base)
-qed
-
 end