| changeset 442 | 13ac1fd0a14d |
| parent 243 | c22b85994e17 |
| child 1479 | 21eb5e156d91 |
| 441:2b97bd6415b7 | 442:13ac1fd0a14d |
|---|---|
15 |
15 |
16 rules |
16 rules |
17 |
17 |
18 (* instance of << for type ['a * 'b] *) |
18 (* instance of << for type ['a * 'b] *) |
19 |
19 |
20 inst_cprod_po "(op <<)::['a * 'b,'a * 'b]=>bool = less_cprod" |
20 inst_cprod_po "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod" |
21 |
21 |
22 end |
22 end |
23 |
23 |
24 |
24 |
25 |
25 |