changeset 47108 | 2a1953f0d20d |
parent 46904 | f30e941b4512 |
child 47761 | dfe747e72fa8 |
--- a/src/HOL/Series.thy Sat Mar 24 16:27:04 2012 +0100 +++ b/src/HOL/Series.thy Sun Mar 25 20:15:39 2012 +0200 @@ -417,8 +417,8 @@ shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)" by (rule geometric_sums [THEN sums_summable]) -lemma half: "0 < 1 / (2::'a::{number_ring,linordered_field_inverse_zero})" - by arith +lemma half: "0 < 1 / (2::'a::linordered_field)" + by simp lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1" proof -