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