author | slotosch |
Mon, 17 Feb 1997 16:50:17 +0100 | |
changeset 2648 | 9944bea3b459 |
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 |