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