src/HOL/Library/List_lexord.thy

 
 instantiation list :: (ord) ord
 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 ..
 
 end
 

 
 instantiation list :: (linorder) distrib_lattice
 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
     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
 

   by (unfold list_le_def, cases x) auto
 
 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"
   by simp_all