author | haftmann |
Wed, 07 Oct 2009 14:01:26 +0200 | |
changeset 32887 | 85e7ab9020ba |
parent 32886 | aba29da80c1b |
child 32888 | ae17e72aac80 |
--- a/src/HOL/Orderings.thy Wed Oct 07 12:06:04 2009 +0200 +++ b/src/HOL/Orderings.thy Wed Oct 07 14:01:26 2009 +0200 @@ -1251,6 +1251,12 @@ lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x" unfolding le_fun_def by simp +lemma bot_boolE: "bot \<Longrightarrow> P" + by (simp add: bot_bool_eq) + +lemma top_boolI: top + by (simp add: top_bool_eq) + text {* Handy introduction and elimination rules for @{text "\<le>"} on unary and binary predicates