src/HOL/Filter.thy
changeset 61245 b77bf45efe21
parent 61233 1da01148d4b1
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Filter.thy	Thu Sep 24 15:21:12 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Fri Sep 25 16:54:31 2015 +0200
     1.3 @@ -390,6 +390,9 @@
     1.4  lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
     1.5    by (simp add: frequently_const_iff)
     1.6  
     1.7 +lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
     1.8 +  by (metis frequentlyE eventually_frequently)
     1.9 +
    1.10  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
    1.11    where "trivial_limit F \<equiv> F = bot"
    1.12