src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 21 16:58:14 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:42 2013 +0100
1.3 @@ -1340,11 +1340,11 @@
1.4
1.5  text {* Some property holds "sufficiently close" to the limit point. *}
1.6
1.7 -lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
1.8 +lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *)
1.9    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
1.10  unfolding eventually_at dist_nz by auto
1.11
1.12 -lemma eventually_within: (* FIXME: this replaces Limits.eventually_within *)
1.13 +lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *)
1.14    "eventually P (at a within S) \<longleftrightarrow>
1.15          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
1.16    by (rule eventually_within_less)
1.17 @@ -1448,12 +1448,12 @@
1.18    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
1.19    { assume "?lhs"
1.20      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
1.21 -      unfolding Limits.eventually_within Limits.eventually_at_topological
1.22 +      unfolding Limits.eventually_within eventually_at_topological
1.23        by auto
1.24      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
1.25        by auto
1.26      then have "?rhs"
1.27 -      unfolding Limits.eventually_at_topological by auto
1.28 +      unfolding eventually_at_topological by auto
1.29    } moreover
1.30    { assume "?rhs" hence "?lhs"
1.31        unfolding Limits.eventually_within
```