--- a/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_lexord.thy Fri Oct 10 06:45:53 2008 +0200
@@ -13,10 +13,10 @@
begin
definition
- list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+ list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
definition
- list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+ list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
instance ..
@@ -63,10 +63,10 @@
begin
definition
- [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+ [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
definition
- [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+ [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
by intro_classes
@@ -92,13 +92,13 @@
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
by (unfold list_le_def) auto
-lemma less_code [code func]:
+lemma less_code [code]:
"xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
"[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
by simp_all
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
"x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
"[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
"(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"