src/HOL/Transcendental.thy
changeset 44710 9caf6883f1f4
parent 44568 e6f291cb5810
child 44725 d3bf0e33c98a
     1.1 --- a/src/HOL/Transcendental.thy	Sun Sep 04 07:15:13 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Sep 04 09:49:45 2011 -0700
     1.3 @@ -1999,7 +1999,7 @@
     1.4  apply (drule tan_total_pos)
     1.5  apply (cut_tac [2] y="-y" in tan_total_pos, safe)
     1.6  apply (rule_tac [3] x = "-x" in exI)
     1.7 -apply (auto intro!: exI)
     1.8 +apply (auto del: exI intro!: exI)
     1.9  done
    1.10  
    1.11  lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
    1.12 @@ -2009,7 +2009,7 @@
    1.13  apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
    1.14  apply (rule_tac [4] Rolle)
    1.15  apply (rule_tac [2] Rolle)
    1.16 -apply (auto intro!: DERIV_tan DERIV_isCont exI
    1.17 +apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
    1.18              simp add: differentiable_def)
    1.19  txt{*Now, simulate TRYALL*}
    1.20  apply (rule_tac [!] DERIV_tan asm_rl)
    1.21 @@ -2785,7 +2785,7 @@
    1.22          have "norm (?diff 1 n - 0) < r" by auto }
    1.23        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
    1.24      qed
    1.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]
    1.26 +    from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
    1.27      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
    1.28      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
    1.29