diff -r a9ed5fcc5e39 -r d41a8ba25b67 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Transcendental.thy	Fri May 29 09:22:56 2009 -0700
@@ -438,7 +438,7 @@
   assumes k: "0 < (k::real)"
   assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   shows "f -- 0 --> 0"
-unfolding LIM_def diff_0_right
+unfolding LIM_eq diff_0_right
 proof (safe)
   let ?h = "of_real (k / 2)::'a"
   have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
@@ -2145,7 +2145,7 @@
 
 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
 apply (cut_tac LIM_cos_div_sin)
-apply (simp only: LIM_def)
+apply (simp only: LIM_eq)
 apply (drule_tac x = "inverse y" in spec, safe, force)
 apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
 apply (rule_tac x = "(pi/2) - e" in exI)