src/HOL/Series.thy
changeset 36349 39be26d1bc28
parent 35028 108662d50512
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Series.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Series.thy	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -381,7 +381,7 @@
     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,division_by_zero,linordered_field})"
     1.8 +lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})"
     1.9    by arith 
    1.10  
    1.11  lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"