--- 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