src/HOL/Lim.thy

--- a/src/HOL/Lim.thy	Fri Jun 05 15:59:20 2009 -0700
+++ b/src/HOL/Lim.thy	Sat Jun 06 09:11:12 2009 -0700
@@ -30,7 +30,7 @@
 subsection {* Limits of Functions *}
 
 lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
-unfolding LIM_def tendsto_def eventually_at ..
+unfolding LIM_def tendsto_iff eventually_at ..
 
 lemma metric_LIM_I:
   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)