src/HOL/Library/List_lexord.thy
changeset 22483 86064f2f2188
parent 22316 f662831459de
child 22744 5cbe966d67a2
     1.1 --- a/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:39 2007 +0100
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:40 2007 +0100
     1.3 @@ -34,6 +34,12 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 +instance list :: (linorder) distrib_lattice
     1.8 +  "inf \<equiv> min"
     1.9 +  "sup \<equiv> max"
    1.10 +  by intro_classes
    1.11 +    (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    1.12 +
    1.13  lemma not_less_Nil [simp]: "\<not> (x < [])"
    1.14    by (unfold list_less_def) simp
    1.15