src/HOL/Library/List_lexord.thy
changeset 28562 4e74209f113e
parent 27682 25aceefd4786
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
     1.8 +  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
     1.9  
    1.10  definition
    1.11 -  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
    1.12 +  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
    1.13  
    1.14  instance ..
    1.15  
    1.16 @@ -63,10 +63,10 @@
    1.17  begin
    1.18  
    1.19  definition
    1.20 -  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    1.21 +  [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    1.22  
    1.23  definition
    1.24 -  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.25 +  [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.26  
    1.27  instance
    1.28    by intro_classes
    1.29 @@ -92,13 +92,13 @@
    1.30  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    1.31    by (unfold list_le_def) auto
    1.32  
    1.33 -lemma less_code [code func]:
    1.34 +lemma less_code [code]:
    1.35    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    1.36    "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
    1.37    "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    1.38    by simp_all
    1.39  
    1.40 -lemma less_eq_code [code func]:
    1.41 +lemma less_eq_code [code]:
    1.42    "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    1.43    "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
    1.44    "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"