| changeset 51542 | 738598beeb26 |
| parent 51115 | 7dbd6832a689 |
| child 52729 | 412c9e0381a1 |
| 51541:e7b6b61b7be2 | 51542:738598beeb26 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Pointwise order on product types *} |
5 header {* Pointwise order on product types *} |
6 |
6 |
7 theory Product_Order |
7 theory Product_Order |
8 imports "~~/src/HOL/Library/Product_plus" |
8 imports Product_plus |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Pointwise ordering *} |
11 subsection {* Pointwise ordering *} |
12 |
12 |
13 instantiation prod :: (ord, ord) ord |
13 instantiation prod :: (ord, ord) ord |