# HG changeset patch
# User haftmann
# Date 1254916886 -7200
# Node ID 85e7ab9020ba7df846d0441c4a4e6ae38902d926
# Parent  aba29da80c1b6fb7b555e2a776d2c5f9b3515ea1
added bot_boolE, top_boolI

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