src/HOL/SEQ.thy
changeset 44282 f0de18b62d63
parent 44208 1d2bf1f240ac
child 44313 d81d57979771
     1.1 --- a/src/HOL/SEQ.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -377,7 +377,7 @@
     1.4  lemma LIMSEQ_mult:
     1.5    fixes a b :: "'a::real_normed_algebra"
     1.6    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
     1.7 -by (rule mult.tendsto)
     1.8 +  by (rule tendsto_mult)
     1.9  
    1.10  lemma increasing_LIMSEQ:
    1.11    fixes f :: "nat \<Rightarrow> real"