# HG changeset patch
# User haftmann
# Date 1255088074 -7200
# Node ID c913cc8316306504bc610f3b15b00cd9b827aebc
# Parent  e871d897969c57c0f93b8839b51fdd0a047af3ec
tuned order of lemmas

diff -r e871d897969c -r c913cc831630 src/HOL/Orderings.thy
--- 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