src/HOL/Filter.thy
changeset 65578 e4997c181cce
parent 63967 2aa42596edc3
child 66162 65cd285f6b9c
     1.1 --- a/src/HOL/Filter.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Filter.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -624,7 +624,7 @@
     1.4    shows "eventually P at_top"
     1.5    using assms by (auto simp: eventually_at_top_linorder)
     1.6  
     1.7 -lemma eventually_ge_at_top:
     1.8 +lemma eventually_ge_at_top [simp]:
     1.9    "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
    1.10    unfolding eventually_at_top_linorder by auto
    1.11  
    1.12 @@ -638,10 +638,10 @@
    1.13    finally show ?thesis .
    1.14  qed
    1.15  
    1.16 -lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
    1.17 +lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
    1.18    unfolding eventually_at_top_dense by auto
    1.19  
    1.20 -lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    1.21 +lemma eventually_gt_at_top [simp]: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    1.22    unfolding eventually_at_top_dense by auto
    1.23  
    1.24  lemma eventually_all_ge_at_top:
    1.25 @@ -664,7 +664,7 @@
    1.26    unfolding at_bot_def
    1.27    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
    1.28  
    1.29 -lemma eventually_le_at_bot:
    1.30 +lemma eventually_le_at_bot [simp]:
    1.31    "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
    1.32    unfolding eventually_at_bot_linorder by auto
    1.33  
    1.34 @@ -678,10 +678,10 @@
    1.35    finally show ?thesis .
    1.36  qed
    1.37  
    1.38 -lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
    1.39 +lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
    1.40    unfolding eventually_at_bot_dense by auto
    1.41  
    1.42 -lemma eventually_gt_at_bot:
    1.43 +lemma eventually_gt_at_bot [simp]:
    1.44    "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
    1.45    unfolding eventually_at_bot_dense by auto
    1.46