src/HOL/Orderings.thy
changeset 22348 ab505d281015
parent 22344 eddeabf16b5d
child 22377 61610b1beedf
     1.1 --- a/src/HOL/Orderings.thy	Fri Feb 23 08:39:20 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Feb 23 08:39:21 2007 +0100
     1.3 @@ -124,8 +124,6 @@
     1.4  
     1.5  class order = preorder + 
     1.6    assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
     1.7 -
     1.8 -context order
     1.9  begin
    1.10  
    1.11  text {* Asymmetry. *}
    1.12 @@ -815,6 +813,13 @@
    1.13  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.14    by (simp add: le_bool_def)
    1.15  
    1.16 +lemma [code func]:
    1.17 +  "False \<le> b \<longleftrightarrow> True"
    1.18 +  "True \<le> b \<longleftrightarrow> b"
    1.19 +  "False < b \<longleftrightarrow> b"
    1.20 +  "True < b \<longleftrightarrow> False"
    1.21 +  unfolding le_bool_def less_bool_def by simp_all
    1.22 +
    1.23  subsection {* Monotonicity, syntactic least value operator and min/max *}
    1.24  
    1.25  locale mono =