src/HOL/Series.thy
changeset 44726 8478eab380e9
parent 44710 9caf6883f1f4
child 44727 d45acd50a894
     1.1 --- a/src/HOL/Series.thy	Mon Sep 05 12:19:04 2011 -0700
     1.2 +++ b/src/HOL/Series.thy	Mon Sep 05 16:07:40 2011 -0700
     1.3 @@ -435,7 +435,7 @@
     1.4  by (simp add: summable_def sums_def convergent_def)
     1.5  
     1.6  lemma summable_LIMSEQ_zero:
     1.7 -  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
     1.9    shows "summable f \<Longrightarrow> f ----> 0"
    1.10  apply (drule summable_convergent_sumr_iff [THEN iffD1])
    1.11  apply (drule convergent_Cauchy)