| author | paulson |
| Thu, 15 May 1997 12:53:12 +0200 | |
| changeset 3194 | 36bfceef1800 |
| parent 2640 | ee4dfce170a0 |
| child 3842 | b55686a7b22c |
| permissions | -rw-r--r-- |
| 2278 | 1 |
(* Title: HOLCF/Up3.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 |
Up3 = Up2 + |
|
12 |
||
| 2640 | 13 |
instance u :: (pcpo)pcpo (least_up,cpo_up) |
| 2278 | 14 |
|
| 2640 | 15 |
constdefs |
16 |
up :: "'a -> ('a)u"
|
|
17 |
"up == (LAM x.Iup(x))" |
|
18 |
fup :: "('a->'c)-> ('a)u -> 'c"
|
|
19 |
"fup == (LAM f p.Ifup(f)(p))" |
|
| 2278 | 20 |
|
21 |
translations |
|
22 |
"case l of up`x => t1" == "fup`(LAM x.t1)`l" |
|
23 |
||
24 |
end |
|
25 |
||
26 |
||
27 |