src/HOL/Orderings.thy
changeset 37767 a2b7a20d6ea3
parent 36960 01594f816e3a
child 38650 f22a564ac820
     1.1 --- a/src/HOL/Orderings.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -264,10 +264,10 @@
     1.4  text {* min/max *}
     1.5  
     1.6  definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.7 -  [code del]: "min a b = (if a \<le> b then a else b)"
     1.8 +  "min a b = (if a \<le> b then a else b)"
     1.9  
    1.10  definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.11 -  [code del]: "max a b = (if a \<le> b then b else a)"
    1.12 +  "max a b = (if a \<le> b then b else a)"
    1.13  
    1.14  lemma min_le_iff_disj:
    1.15    "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    1.16 @@ -1196,10 +1196,10 @@
    1.17  begin
    1.18  
    1.19  definition
    1.20 -  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    1.21 +  le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    1.22  
    1.23  definition
    1.24 -  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.25 +  less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.26  
    1.27  definition
    1.28    top_bool_eq: "top = True"
    1.29 @@ -1244,10 +1244,10 @@
    1.30  begin
    1.31  
    1.32  definition
    1.33 -  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.34 +  le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.35  
    1.36  definition
    1.37 -  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    1.38 +  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    1.39  
    1.40  instance ..
    1.41