# 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) \ (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 \ x" and ygt0: "0 \ y" and sq: "x^2 \ y^2" - shows "x \ y" -proof - - from sq have "x ^ Suc (Suc 0) \ y ^ Suc (Suc 0)" - by (simp only: numeral_2_eq_2) - thus "x \ y" using ygt0 - by (rule power_le_imp_le_base) -qed - end