diff -r aba29da80c1b -r 85e7ab9020ba src/HOL/Orderings.thy
--- 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