| changeset 442 | 13ac1fd0a14d |
| parent 243 | c22b85994e17 |
| child 752 | b89462f9d5f1 |
| 441:2b97bd6415b7 | 442:13ac1fd0a14d |
|---|---|
17 |
17 |
18 rules |
18 rules |
19 |
19 |
20 (* instance of << for type ['a -> 'b] *) |
20 (* instance of << for type ['a -> 'b] *) |
21 |
21 |
22 inst_cfun_po "(op <<)::['a->'b,'a->'b]=>bool = less_cfun" |
22 inst_cfun_po "((op <<)::['a->'b,'a->'b]=>bool) = less_cfun" |
23 |
23 |
24 (* definitions *) |
24 (* definitions *) |
25 (* The least element in type 'a->'b *) |
25 (* The least element in type 'a->'b *) |
26 |
26 |
27 UU_cfun_def "UU_cfun == fabs(% x.UU)" |
27 UU_cfun_def "UU_cfun == fabs(% x.UU)" |