src/HOL/SEQ.thy
changeset 36650 d65f07abfa7c
parent 36647 edc381bf7200
child 36663 f75b13ed4898
     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