src/HOL/Transcendental.thy

 next
   assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
     unfolding isCont_def
     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
-                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
+                intro!: exI[of _ "\<bar>x\<bar>"])
 qed
 
 lemma tendsto_ln [tendsto_intros]:
   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   by (rule isCont_tendsto_compose [OF isCont_ln])

   proof (rule filterlim_mono_eventually)
     show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
       unfolding eventually_at_right[OF zero_less_one]
       using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
   qed (simp_all add: at_eq_sup_left_right)
-qed (simp add: tendsto_const)
+qed simp
 
 lemma tendsto_exp_limit_at_top:
   fixes x :: real
   shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
   apply (subst filterlim_at_top_to_right)

   assumes "\<bar>x\<bar> \<le> 1"
   shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
 proof (cases "x = 0")
   case True
   thus ?thesis
-    unfolding One_nat_def by (auto simp add: tendsto_const)
+    unfolding One_nat_def by auto
 next
   case False
   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
   show "?a ----> 0"
   proof (cases "\<bar>x\<bar> < 1")