deleted comments
authorobua
Thu Jun 07 17:21:43 2007 +0200 (2007-06-07)
changeset 2329377577fc2f141
parent 23292 1c39f1bd1f53
child 23294 9302a50a5bc9
deleted comments
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Jun 07 14:26:05 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jun 07 17:21:43 2007 +0200
     1.3 @@ -28,32 +28,6 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -(*lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
     1.8 -by simp
     1.9 -
    1.10 -lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
    1.11 -by simp
    1.12 -
    1.13 -text{*Legacy: weaker version of the theorem @{text power_strict_mono}*}
    1.14 -lemma realpow_less:
    1.15 -     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.16 -thm power_strict_mono
    1.17 -apply (rule power_strict_mono, auto) 
    1.18 -done *)
    1.19 -
    1.20 -(* declare [simp del]: zero_le_power
    1.21 -
    1.22 -lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
    1.23 -by (simp)
    1.24 -
    1.25 -
    1.26 -lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
    1.27 -by (simp)
    1.28 -
    1.29 -lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
    1.30 -by (simp)
    1.31 -
    1.32 -*)
    1.33  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
    1.34  by (rule power_increasing[of 0 n "2::real", simplified])
    1.35