added bot_boolE, top_boolI
authorhaftmann
Wed Oct 07 14:01:26 2009 +0200 (2009-10-07)
changeset 3288785e7ab9020ba
parent 32886 aba29da80c1b
child 32888 ae17e72aac80
added bot_boolE, top_boolI
src/HOL/Orderings.thy
     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