src/HOL/Library/Product_ord.thy
changeset 22483 86064f2f2188
parent 22177 515021e98684
child 22744 5cbe966d67a2
     1.1 --- a/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:39 2007 +0100
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:40 2007 +0100
     1.3 @@ -31,4 +31,10 @@
     1.4  instance * :: (linorder, linorder) linorder
     1.5    by default (auto simp: prod_le_def)
     1.6  
     1.7 +instance * :: (linorder, linorder) distrib_lattice
     1.8 +  inf_prod_def: "inf \<equiv> min"
     1.9 +  sup_prod_def: "sup \<equiv> max"
    1.10 +  by intro_classes
    1.11 +    (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    1.12 +
    1.13  end