# HG changeset patch
# User wenzelm
# Date 1272997613 -7200
# Node ID d65f07abfa7c512674fe898850a48d4d8fa98bcc
# Parent  bfd8c550faa69d139eefb4b76901ea5ffc8ef67a
fixed proof (cf. edc381bf7200);

diff -r bfd8c550faa6 -r d65f07abfa7c src/HOL/SEQ.thy
--- 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)