src/HOL/Series.thy

--- a/src/HOL/Series.thy	Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Series.thy	Mon Apr 26 15:37:50 2010 +0200
@@ -381,7 +381,7 @@
   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,division_ring_inverse_zero,linordered_field})"
+lemma half: "0 < 1 / (2::'a::{number_ring,linordered_field_inverse_zero})"
   by arith 
 
 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"