src/HOL/Series.thy
changeset 60141 833adf7db7d8
parent 59741 5b762cd73a8e
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Series.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/Series.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -643,7 +643,7 @@
     1.4      by (simp only: setsum_diff finite_S1 S2_le_S1)
     1.5  
     1.6    with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
     1.7 -    by (rule LIMSEQ_diff_approach_zero2)
     1.8 +    by (rule Lim_transform2)
     1.9    thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
    1.10  qed
    1.11