--- a/src/HOL/Orderings.thy Fri Oct 09 10:00:47 2009 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 09 13:34:34 2009 +0200
@@ -1179,16 +1179,22 @@
end
lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
-by (simp add: le_bool_def)
+ by (simp add: le_bool_def)
lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
-by (simp add: le_bool_def)
+ by (simp add: le_bool_def)
lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-by (simp add: le_bool_def)
+ by (simp add: le_bool_def)
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
-by (simp add: le_bool_def)
+ by (simp add: le_bool_def)
+
+lemma bot_boolE: "bot \<Longrightarrow> P"
+ by (simp add: bot_bool_eq)
+
+lemma top_boolI: top
+ by (simp add: top_bool_eq)
lemma [code]:
"False \<le> b \<longleftrightarrow> True"
@@ -1251,12 +1257,6 @@
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