# HG changeset patch
# User huffman
# Date 1244161711 25200
# Node ID 29090e3111bd5cd3bb599a2f934f77d37a37020b
# Parent  97bab1ac463efb6e31ee252a5486676c46eb265f
define netlimit in terms of eventually

diff -r 97bab1ac463e -r 29090e3111bd src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 17:24:09 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 17:28:31 2009 -0700
@@ -1619,7 +1619,7 @@
 
 definition
   netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
-  "netlimit net = (SOME a. \<forall>r>0. \<exists>A\<in>Rep_net net. \<forall>x\<in>A. dist x a < r)"
+  "netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"
 
 lemma dist_triangle3:
   fixes x y :: "'a::metric_space"
@@ -1632,8 +1632,7 @@
   shows "netlimit (at a within S) = a"
 using assms
 apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def eventually_def [symmetric])
-apply (simp add: eventually_within zero_less_dist_iff)
+apply (simp add: netlimit_def eventually_within zero_less_dist_iff)
 apply (rule some_equality, fast)
 apply (rename_tac b)
 apply (rule ccontr)