--- 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.
--- 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