1.1 --- a/src/HOL/SEQ.thy	Sun Sep 04 07:15:13 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Sep 04 09:49:45 2011 -0700
     1.3 @@ -380,22 +380,6 @@
     1.4    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
     1.5  unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
     1.6  
     1.7 -lemma LIMSEQ_add_const: (* FIXME: delete *)
     1.8 -  fixes a :: "'a::real_normed_vector"
     1.9 -  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
    1.10 -by (intro tendsto_intros)
    1.11 -
    1.12 -(* FIXME: delete *)
    1.13 -lemma LIMSEQ_add_minus:
    1.14 -  fixes a b :: "'a::real_normed_vector"
    1.15 -  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
    1.16 -by (intro tendsto_intros)
    1.17 -
    1.18 -lemma LIMSEQ_diff_const: (* FIXME: delete *)
    1.19 -  fixes a b :: "'a::real_normed_vector"
    1.20 -  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
    1.21 -by (intro tendsto_intros)
    1.22 -
    1.23  lemma LIMSEQ_diff_approach_zero:
    1.24    fixes L :: "'a::real_normed_vector"
    1.25    shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    1.26 @@ -438,7 +422,8 @@
    1.27  
    1.28  lemma LIMSEQ_inverse_real_of_nat_add_minus:
    1.29       "(%n. r + -inverse(real(Suc n))) ----> r"
    1.30 -  using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
    1.31 +  using tendsto_add [OF tendsto_const
    1.32 +    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
    1.33  
    1.34  lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
    1.35       "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"