diff -r 6026c14f5e5d -r b77bf45efe21 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Sep 24 15:21:12 2015 +0200
+++ b/src/HOL/Filter.thy	Fri Sep 25 16:54:31 2015 +0200
@@ -390,6 +390,9 @@
 lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
   by (simp add: frequently_const_iff)
 
+lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
+  by (metis frequentlyE eventually_frequently)
+
 abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   where "trivial_limit F \<equiv> F = bot"