| 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)u *) |
18 (* instance of << for type ('a)u *) |
19 |
19 |
20 inst_lift_po "(op <<)::[('a)u,('a)u]=>bool = less_lift" |
20 inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" |
21 |
21 |
22 end |
22 end |
23 |
23 |
24 |
24 |
25 |
25 |