--- a/src/HOL/Library/List_lexord.thy Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/Library/List_lexord.thy Sun May 06 21:50:17 2007 +0200
@@ -13,7 +13,7 @@
list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
-lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
+lemmas list_ord_defs [code func del] = list_less_def list_le_def
instance list :: (order) order
apply (intro_classes, unfold list_ord_defs)
@@ -40,7 +40,7 @@
by intro_classes
(auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
-lemmas [code nofunc] = inf_list_def sup_list_def
+lemmas [code func del] = inf_list_def sup_list_def
lemma not_less_Nil [simp]: "\<not> (x < [])"
by (unfold list_less_def) simp