changeset 1476 | 608483c2122a |
parent 1440 | de6f18da81bb |
1475:7f5a4cd08209 | 1476:608483c2122a |
---|---|
21 le_fun_def "f [= g == ALL x. f x [= g x" |
21 le_fun_def "f [= g == ALL x. f x [= g x" |
22 |
22 |
23 |
23 |
24 (* duals *) |
24 (* duals *) |
25 |
25 |
26 subtype |
26 typedef |
27 'a dual = "{x::'a. True}" |
27 'a dual = "{x::'a. True}" |
28 |
28 |
29 instance |
29 instance |
30 dual :: (le) le |
30 dual :: (le) le |
31 |
31 |