| changeset 3323 | 194ae2e0c193 |
| parent 2840 | 7e03e61612b0 |
| child 12030 | 46d57d0290a2 |
| 3322:bc4d107fb6dd | 3323:194ae2e0c193 |
|---|---|
10 |
10 |
11 Cprod1 = Cfun3 + |
11 Cprod1 = Cfun3 + |
12 |
12 |
13 default cpo |
13 default cpo |
14 |
14 |
15 instance "*"::(sq_ord,sq_ord)sq_ord |
|
16 |
|
15 defs |
17 defs |
16 |
18 |
17 less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)" |
19 less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)" |
18 |
20 |
19 end |
21 end |