src/HOL/Limits.thy

--- a/src/HOL/Limits.thy	Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Limits.thy	Wed Feb 20 12:04:42 2013 +0100
@@ -264,6 +264,9 @@
 lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   by (rule eventually_False [symmetric])
 
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+  by (cases P) (simp_all add: eventually_False)
+
 
 subsection {* Map function for filters *}