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