src/HOL/Real/RealPow.thy
changeset 25875 536dfdc25e0a
parent 23477 f4b83f03cac9
child 26565 522f45a8604e
     1.1 --- a/src/HOL/Real/RealPow.thy	Wed Jan 09 19:23:36 2008 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Wed Jan 09 19:23:50 2008 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  
     1.6  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
     1.7 -by (rule power_increasing[of 0 n "2::real", simplified])
     1.8 +by simp
     1.9  
    1.10  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
    1.11  apply (induct "n")