fixed proof (cf. edc381bf7200);
authorwenzelm
Tue May 04 20:26:53 2010 +0200 (2010-05-04)
changeset 36650d65f07abfa7c
parent 36649 bfd8c550faa6
child 36653 8629ac3efb19
fixed proof (cf. edc381bf7200);
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/SEQ.thy	Tue May 04 18:19:24 2010 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Tue May 04 20:26:53 2010 +0200
     1.3 @@ -547,7 +547,7 @@
     1.4    assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
     1.5    shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
     1.6  proof (cases "finite A")
     1.7 -  case True with assms show ?thesis
     1.8 +  case True from this and assms show ?thesis
     1.9      by (induct A set: finite) (simp_all add: convergent_const convergent_add)
    1.10  qed (simp add: convergent_const)
    1.11