--- a/src/HOL/Series.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Series.thy Mon Nov 09 19:42:33 2009 +0100
@@ -293,11 +293,11 @@
have "convergent (\<lambda>n. setsum f {0..<n})"
proof (rule Bseq_mono_convergent)
show "Bseq (\<lambda>n. setsum f {0..<n})"
- by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+ by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
(auto simp add: le pos)
next
show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
- by (auto intro: setsum_mono2 pos)
+ by (auto intro: setsum_mono2 pos)
qed
then obtain L where "(%n. setsum f {0..<n}) ----> L"
by (blast dest: convergentD)