diff -r 33439faadd67 -r 8321948340ea src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Limits.thy	Sat Aug 20 06:34:51 2011 -0700
@@ -216,6 +216,13 @@
   "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
 
+abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
+  where "trivial_limit F \<equiv> F = bot"
+
+lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
+  by (rule eventually_False [symmetric])
+
+
 subsection {* Map function for filters *}
 
 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
@@ -259,9 +266,11 @@
   then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
 qed auto
 
-lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   unfolding filter_eq_iff eventually_sequentially by auto
 
+lemmas trivial_limit_sequentially = sequentially_bot
+
 lemma eventually_False_sequentially [simp]:
   "\<not> eventually (\<lambda>n. False) sequentially"
   by (simp add: eventually_False)
@@ -272,12 +281,6 @@
   by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
 
 
-definition trivial_limit :: "'a filter \<Rightarrow> bool"
-  where "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
-
-lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
-  by (auto simp add: trivial_limit_def eventually_sequentially)
-
 subsection {* Standard filters *}
 
 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)