equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/lift3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 |
|
7 Class instance of ('a)u for class pcpo |
|
8 |
|
9 *) |
|
10 |
|
11 Lift3 = Lift2 + |
|
12 |
|
13 arities "u" :: (pcpo)pcpo (* Witness lift2.ML *) |
|
14 |
|
15 consts |
|
16 up :: "'a -> ('a)u" |
|
17 lift :: "('a->'c)-> ('a)u -> 'c" |
|
18 |
|
19 rules |
|
20 |
|
21 inst_lift_pcpo "UU::('a)u = UU_lift" |
|
22 |
|
23 up_def "up == (LAM x.Iup(x))" |
|
24 lift_def "lift == (LAM f p.Ilift(f)(p))" |
|
25 |
|
26 end |
|
27 |
|
28 |
|
29 |