src/HOL/Library/Product_Order.thy
changeset 58881 b9556a055632
parent 56218 1c3f1f2431f9
child 60500 903bb1495239
equal deleted inserted replaced
58880:0baae4311a9f 58881:b9556a055632
     1 (*  Title:      HOL/Library/Product_Order.thy
     1 (*  Title:      HOL/Library/Product_Order.thy
     2     Author:     Brian Huffman
     2     Author:     Brian Huffman
     3 *)
     3 *)
     4 
     4 
     5 header {* Pointwise order on product types *}
     5 section {* Pointwise order on product types *}
     6 
     6 
     7 theory Product_Order
     7 theory Product_Order
     8 imports Product_plus Conditionally_Complete_Lattices
     8 imports Product_plus Conditionally_Complete_Lattices
     9 begin
     9 begin
    10 
    10