--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Apr 25 16:23:40 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Apr 25 20:48:19 2010 -0700
@@ -976,15 +976,6 @@
text{* Prove That They are all nets. *}
-(* TODO: move to HOL/Limits.thy *)
-lemma expand_net_eq:
- "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
- unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
-
-(* TODO: move to HOL/Limits.thy *)
-lemma within_UNIV: "net within UNIV = net"
- unfolding expand_net_eq eventually_within by simp
-
lemma eventually_at_infinity:
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
unfolding at_infinity_def