--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Aug 20 06:34:51 2011 -0700
@@ -966,13 +966,8 @@
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
-lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
- unfolding trivial_limit_def ..
-
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
- apply (safe elim!: trivial_limit_eventually)
- apply (simp add: eventually_False [symmetric])
- done
+ by (simp add: filter_eq_iff)
text{* Combining theorems for "eventually" *}