src/HOL/Orderings.thy
changeset 28562 4e74209f113e
parent 28516 e6fdcaaadbd3
child 28685 275122631271
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -968,10 +968,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     1.8 +  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     1.9  
    1.10  definition
    1.11 -  less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
    1.12 +  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
    1.13  
    1.14  instance
    1.15    by intro_classes (auto simp add: le_bool_def less_bool_def)
    1.16 @@ -990,7 +990,7 @@
    1.17  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.18  by (simp add: le_bool_def)
    1.19  
    1.20 -lemma [code func]:
    1.21 +lemma [code]:
    1.22    "False \<le> b \<longleftrightarrow> True"
    1.23    "True \<le> b \<longleftrightarrow> b"
    1.24    "False < b \<longleftrightarrow> b"
    1.25 @@ -1004,10 +1004,10 @@
    1.26  begin
    1.27  
    1.28  definition
    1.29 -  le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.30 +  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.31  
    1.32  definition
    1.33 -  less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
    1.34 +  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
    1.35  
    1.36  instance ..
    1.37