changeset 32887 | 85e7ab9020ba |
parent 32215 | 87806301a813 |
child 32899 | c913cc831630 |
--- 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