1.1 --- a/NEWS Tue May 11 11:58:34 2010 -0700
1.2 +++ b/NEWS Tue May 11 12:05:19 2010 -0700
1.3 @@ -143,7 +143,11 @@
1.4 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
1.5 no longer shadowed. INCOMPATIBILITY.
1.6
1.7 -* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY.
1.8 +* Dropped theorem duplicate comp_arith; use semiring_norm instead.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 +* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
1.12 +INCOMPATIBILITY.
1.13
1.14 * Theory 'Finite_Set': various folding_* locales facilitate the application
1.15 of the various fold combinators on finite sets.
2.1 --- a/src/HOL/RealPow.thy Tue May 11 11:58:34 2010 -0700
2.2 +++ b/src/HOL/RealPow.thy Tue May 11 12:05:19 2010 -0700
2.3 @@ -88,17 +88,4 @@
2.4 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
2.5 by (auto simp add: power2_eq_square)
2.6
2.7 -(* The following theorem is by Benjamin Porter *)
2.8 -(* TODO: no longer real-specific; rename and move elsewhere *)
2.9 -lemma real_sq_order:
2.10 - fixes x :: "'a::linordered_semidom"
2.11 - assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
2.12 - shows "x \<le> y"
2.13 -proof -
2.14 - from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
2.15 - by (simp only: numeral_2_eq_2)
2.16 - thus "x \<le> y" using ygt0
2.17 - by (rule power_le_imp_le_base)
2.18 -qed
2.19 -
2.20 end