| changeset 3323 | 194ae2e0c193 |
| parent 2640 | ee4dfce170a0 |
| child 12030 | 46d57d0290a2 |
| 3322:bc4d107fb6dd | 3323:194ae2e0c193 |
|---|---|
6 Partial ordering for the strict product |
6 Partial ordering for the strict product |
7 *) |
7 *) |
8 |
8 |
9 Sprod1 = Sprod0 + |
9 Sprod1 = Sprod0 + |
10 |
10 |
11 instance "**"::(sq_ord,sq_ord)sq_ord |
|
12 |
|
11 defs |
13 defs |
12 less_sprod_def "less p1 p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
14 less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
13 |
15 |
14 end |
16 end |