src/HOL/Library/List_lexord.thy
changeset 22744 5cbe966d67a2
parent 22483 86064f2f2188
child 22845 5f9138bcb3d7
     1.1 --- a/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:41 2007 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:42 2007 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
     1.5    list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
     1.6  
     1.7 -lemmas list_ord_defs = list_less_def list_le_def
     1.8 +lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
     1.9  
    1.10  instance list :: (order) order
    1.11    apply (intro_classes, unfold list_ord_defs)
    1.12 @@ -40,6 +40,8 @@
    1.13    by intro_classes
    1.14      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    1.15  
    1.16 +lemmas [code nofunc] = inf_list_def sup_list_def
    1.17 +
    1.18  lemma not_less_Nil [simp]: "\<not> (x < [])"
    1.19    by (unfold list_less_def) simp
    1.20