src/HOL/Orderings.thy
changeset 32899 c913cc831630
parent 32887 85e7ab9020ba
child 32960 69916a850301
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 09 10:00:47 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 09 13:34:34 2009 +0200
     1.3 @@ -1179,16 +1179,22 @@
     1.4  end
     1.5  
     1.6  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
     1.7 -by (simp add: le_bool_def)
     1.8 +  by (simp add: le_bool_def)
     1.9  
    1.10  lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    1.11 -by (simp add: le_bool_def)
    1.12 +  by (simp add: le_bool_def)
    1.13  
    1.14  lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.15 -by (simp add: le_bool_def)
    1.16 +  by (simp add: le_bool_def)
    1.17  
    1.18  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.19 -by (simp add: le_bool_def)
    1.20 +  by (simp add: le_bool_def)
    1.21 +
    1.22 +lemma bot_boolE: "bot \<Longrightarrow> P"
    1.23 +  by (simp add: bot_bool_eq)
    1.24 +
    1.25 +lemma top_boolI: top
    1.26 +  by (simp add: top_bool_eq)
    1.27  
    1.28  lemma [code]:
    1.29    "False \<le> b \<longleftrightarrow> True"
    1.30 @@ -1251,12 +1257,6 @@
    1.31  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
    1.32    unfolding le_fun_def by simp
    1.33  
    1.34 -lemma bot_boolE: "bot \<Longrightarrow> P"
    1.35 -  by (simp add: bot_bool_eq)
    1.36 -
    1.37 -lemma top_boolI: top
    1.38 -  by (simp add: top_bool_eq)
    1.39 -
    1.40  text {*
    1.41    Handy introduction and elimination rules for @{text "\<le>"}
    1.42    on unary and binary predicates