| changeset 442 | 13ac1fd0a14d |
| parent 243 | c22b85994e17 |
| child 1168 | 74be52691d62 |
| 441:2b97bd6415b7 | 442:13ac1fd0a14d |
|---|---|
16 up :: "'a -> ('a)u" |
16 up :: "'a -> ('a)u" |
17 lift :: "('a->'c)-> ('a)u -> 'c" |
17 lift :: "('a->'c)-> ('a)u -> 'c" |
18 |
18 |
19 rules |
19 rules |
20 |
20 |
21 inst_lift_pcpo "UU::('a)u = UU_lift" |
21 inst_lift_pcpo "(UU::('a)u) = UU_lift" |
22 |
22 |
23 up_def "up == (LAM x.Iup(x))" |
23 up_def "up == (LAM x.Iup(x))" |
24 lift_def "lift == (LAM f p.Ilift(f)(p))" |
24 lift_def "lift == (LAM f p.Ilift(f)(p))" |
25 |
25 |
26 end |
26 end |