1.1 --- a/NEWS	Sun Sep 04 07:15:13 2011 -0700
     1.2 +++ b/NEWS	Sun Sep 04 09:49:45 2011 -0700
     1.3 @@ -296,6 +296,9 @@
     1.4    LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
     1.5    LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
     1.6    LIMSEQ_imp_rabs ~> tendsto_rabs
     1.7 +  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
     1.8 +  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
     1.9 +  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
    1.10    LIM_ident ~> tendsto_ident_at
    1.11    LIM_const ~> tendsto_const
    1.12    LIM_add ~> tendsto_add

     2.1 --- a/src/HOL/SEQ.thy	Sun Sep 04 07:15:13 2011 -0700
     2.2 +++ b/src/HOL/SEQ.thy	Sun Sep 04 09:49:45 2011 -0700
     2.3 @@ -380,22 +380,6 @@
     2.4    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
     2.5  unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
     2.6  
     2.7 -lemma LIMSEQ_add_const: (* FIXME: delete *)
     2.8 -  fixes a :: "'a::real_normed_vector"
     2.9 -  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
    2.10 -by (intro tendsto_intros)
    2.11 -
    2.12 -(* FIXME: delete *)
    2.13 -lemma LIMSEQ_add_minus:
    2.14 -  fixes a b :: "'a::real_normed_vector"
    2.15 -  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
    2.16 -by (intro tendsto_intros)
    2.17 -
    2.18 -lemma LIMSEQ_diff_const: (* FIXME: delete *)
    2.19 -  fixes a b :: "'a::real_normed_vector"
    2.20 -  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
    2.21 -by (intro tendsto_intros)
    2.22 -
    2.23  lemma LIMSEQ_diff_approach_zero:
    2.24    fixes L :: "'a::real_normed_vector"
    2.25    shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    2.26 @@ -438,7 +422,8 @@
    2.27  
    2.28  lemma LIMSEQ_inverse_real_of_nat_add_minus:
    2.29       "(%n. r + -inverse(real(Suc n))) ----> r"
    2.30 -  using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
    2.31 +  using tendsto_add [OF tendsto_const
    2.32 +    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
    2.33  
    2.34  lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
    2.35       "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"

     3.1 --- a/src/HOL/Series.thy	Sun Sep 04 07:15:13 2011 -0700
     3.2 +++ b/src/HOL/Series.thy	Sun Sep 04 09:49:45 2011 -0700
     3.3 @@ -122,7 +122,7 @@
     3.4    shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
     3.5    apply (unfold sums_def)
     3.6    apply (simp add: sumr_offset)
     3.7 -  apply (rule LIMSEQ_diff_const)
     3.8 +  apply (rule tendsto_diff [OF _ tendsto_const])
     3.9    apply (rule LIMSEQ_ignore_initial_segment)
    3.10    apply assumption
    3.11  done
    3.12 @@ -166,7 +166,7 @@
    3.13  proof -
    3.14    from sumSuc[unfolded sums_def]
    3.15    have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
    3.16 -  from LIMSEQ_add_const[OF this, where b="f 0"]
    3.17 +  from tendsto_add[OF this tendsto_const, where b="f 0"]
    3.18    have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
    3.19    thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
    3.20  qed
    3.21 @@ -625,7 +625,7 @@
    3.22   apply (simp add:diff_Suc split:nat.splits)
    3.23   apply (blast intro: norm_ratiotest_lemma)
    3.24  apply (rule_tac x = "Suc N" in exI, clarify)
    3.25 -apply(simp cong:setsum_ivl_cong)
    3.26 +apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
    3.27  done
    3.28  
    3.29  lemma ratio_test:

     4.1 --- a/src/HOL/Transcendental.thy	Sun Sep 04 07:15:13 2011 -0700
     4.2 +++ b/src/HOL/Transcendental.thy	Sun Sep 04 09:49:45 2011 -0700
     4.3 @@ -1999,7 +1999,7 @@
     4.4  apply (drule tan_total_pos)
     4.5  apply (cut_tac [2] y="-y" in tan_total_pos, safe)
     4.6  apply (rule_tac [3] x = "-x" in exI)
     4.7 -apply (auto intro!: exI)
     4.8 +apply (auto del: exI intro!: exI)
     4.9  done
    4.10  
    4.11  lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
    4.12 @@ -2009,7 +2009,7 @@
    4.13  apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
    4.14  apply (rule_tac [4] Rolle)
    4.15  apply (rule_tac [2] Rolle)
    4.16 -apply (auto intro!: DERIV_tan DERIV_isCont exI
    4.17 +apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
    4.18              simp add: differentiable_def)
    4.19  txt{*Now, simulate TRYALL*}
    4.20  apply (rule_tac [!] DERIV_tan asm_rl)
    4.21 @@ -2785,7 +2785,7 @@
    4.22          have "norm (?diff 1 n - 0) < r" by auto }
    4.23        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
    4.24      qed
    4.25 -    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
    4.26 +    from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
    4.27      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
    4.28      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
    4.29