--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 12 10:28:45 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 12 10:43:36 2011 -0700
@@ -963,9 +963,6 @@
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_iff eventually_at)
-lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
- unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
-
lemma Lim_at_infinity:
"(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
by (auto simp add: tendsto_iff eventually_at_infinity)