src/HOL/Orderings.thy
changeset 32887 85e7ab9020ba
parent 32215 87806301a813
child 32899 c913cc831630
     1.1 --- a/src/HOL/Orderings.thy	Wed Oct 07 12:06:04 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Oct 07 14:01:26 2009 +0200
     1.3 @@ -1251,6 +1251,12 @@
     1.4  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
     1.5    unfolding le_fun_def by simp
     1.6  
     1.7 +lemma bot_boolE: "bot \<Longrightarrow> P"
     1.8 +  by (simp add: bot_bool_eq)
     1.9 +
    1.10 +lemma top_boolI: top
    1.11 +  by (simp add: top_bool_eq)
    1.12 +
    1.13  text {*
    1.14    Handy introduction and elimination rules for @{text "\<le>"}
    1.15    on unary and binary predicates