--- a/src/HOL/Hyperreal/Series.thy Sat Jul 29 00:51:36 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Sat Jul 29 13:15:12 2006 +0200
@@ -323,6 +323,8 @@
lemmas sumr_geometric = geometric_sum [where 'a = real]
+ML {* fast_arith_split_limit := 0; *} (* FIXME: needed because otherwise a premise gets simplified away *)
+
lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
apply (case_tac "x = 1")
apply (auto dest!: LIMSEQ_rabs_realpow_zero2
@@ -333,6 +335,8 @@
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
done
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
+
text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
lemma summable_convergent_sumr_iff: