src/HOL/Series.thy
changeset 36660 1cc4ab4b7ff7
parent 36657 f376af79f6b7
child 41970 47d6e13d1710
--- a/src/HOL/Series.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Series.thy	Tue May 04 10:06:05 2010 -0700
@@ -100,7 +100,7 @@
 
 lemma summable_sums: "summable f ==> f sums (suminf f)"
 apply (simp add: summable_def suminf_def sums_def)
-apply (blast intro: theI LIMSEQ_unique)
+apply (fast intro: theI LIMSEQ_unique)
 done
 
 lemma summable_sumr_LIMSEQ_suminf: 
@@ -701,7 +701,7 @@
     apply (auto simp add: norm_mult_ineq)
     done
   hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
-    unfolding LIMSEQ_conv_tendsto tendsto_Zfun_iff diff_0_right
+    unfolding tendsto_Zfun_iff diff_0_right
     by (simp only: setsum_diff finite_S1 S2_le_S1)
 
   with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"