Removed junk
authornipkow
Sun May 13 09:23:27 2007 +0200 (2007-05-13)
changeset 229452863582c61b5
parent 22944 1d471b8dec4e
child 22946 9793d28d49ad
Removed junk
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/RealPow.thy	Sun May 13 07:11:21 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Sun May 13 09:23:27 2007 +0200
     1.3 @@ -235,14 +235,4 @@
     1.4  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
     1.5  by (case_tac "n", auto)
     1.6  
     1.7 -lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
     1.8 -by (simp add: zero_less_power)
     1.9 -
    1.10 -lemma lemma_realpow_num_two_mono:
    1.11 -     "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
    1.12 -apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
    1.13 -apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
    1.14 -apply (auto simp add: realpow_num_eq_if)
    1.15 -done
    1.16 -
    1.17  end