diff -r e2b06bfe471a -r 5cbe966d67a2 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:42 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 = list_less_def list_le_def
+lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
 
 instance list :: (order) order
   apply (intro_classes, unfold list_ord_defs)
@@ -40,6 +40,8 @@
   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
+
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp