# HG changeset patch
# User hoelzl
# Date 1272988400 -7200
# Node ID edc381bf72006af2a21395fa2d9be749695cdacc
# Parent  8687bc6608d601c7e65f69e8c7ae99a44df0bd05
Removed unnecessary assumption

diff -r 8687bc6608d6 -r edc381bf7200 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue May 04 16:25:16 2010 +0200
+++ b/src/HOL/SEQ.thy	Tue May 04 17:53:20 2010 +0200
@@ -544,10 +544,12 @@
 
 lemma convergent_setsum:
   fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
-  assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
   shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
-using assms
-by (induct A set: finite, simp_all add: convergent_const convergent_add)
+proof (cases "finite A")
+  case True with assms show ?thesis
+    by (induct A set: finite) (simp_all add: convergent_const convergent_add)
+qed (simp add: convergent_const)
 
 lemma (in bounded_linear) convergent:
   assumes "convergent (\<lambda>n. X n)"