| author | paulson |
| Tue, 18 Mar 1997 10:42:08 +0100 | |
| changeset 2802 | f119c3686782 |
| 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 |