fixed proof (cf. edc381bf7200);
--- a/src/HOL/SEQ.thy Tue May 04 18:19:24 2010 +0200
+++ b/src/HOL/SEQ.thy Tue May 04 20:26:53 2010 +0200
@@ -547,7 +547,7 @@
assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
proof (cases "finite A")
- case True with assms show ?thesis
+ case True from this and assms show ?thesis
by (induct A set: finite) (simp_all add: convergent_const convergent_add)
qed (simp add: convergent_const)