| changeset 15576 | efb95d0d01f7 |
| parent 15575 | 63babb1ee883 |
| child 15577 | e16da3068ad6 |
| 15575:63babb1ee883 | 15576:efb95d0d01f7 |
|---|---|
1 (* Title: HOLCF/Up3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 |
|
5 Class instance of ('a)u for class pcpo |
|
6 *) |
|
7 |
|
8 Up3 = Up2 + |
|
9 |
|
10 instance u :: (pcpo)pcpo (least_up,cpo_up) |
|
11 |
|
12 constdefs |
|
13 up :: "'a -> ('a)u" |
|
14 "up == (LAM x. Iup(x))" |
|
15 fup :: "('a->'c)-> ('a)u -> 'c" |
|
16 "fup == (LAM f p. Ifup(f)(p))" |
|
17 |
|
18 translations |
|
19 "case l of up$x => t1" == "fup$(LAM x. t1)$l" |
|
20 |
|
21 end |
|
22 |
|
23 |
|
24 |