| author | wenzelm |
| Thu Aug 27 20:46:36 1998 +0200 (1998-08-27) | |
| changeset 5400 | 645f46a24c72 |
| parent 243 | c22b85994e17 |
| permissions | -rw-r--r-- |
| nipkow@243 | 1 |
(* Title: HOLCF/cfun3.thy |
| nipkow@243 | 2 |
ID: $Id$ |
| nipkow@243 | 3 |
Author: Franz Regensburger |
| nipkow@243 | 4 |
Copyright 1993 Technische Universitaet Muenchen |
| nipkow@243 | 5 |
|
| nipkow@243 | 6 |
Class instance of -> for class pcpo |
| nipkow@243 | 7 |
|
| nipkow@243 | 8 |
*) |
| nipkow@243 | 9 |
|
| nipkow@243 | 10 |
Cfun3 = Cfun2 + |
| nipkow@243 | 11 |
|
| nipkow@243 | 12 |
arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *) |
| nipkow@243 | 13 |
|
| nipkow@243 | 14 |
consts |
| nipkow@243 | 15 |
Istrictify :: "('a->'b)=>'a=>'b"
|
| nipkow@243 | 16 |
strictify :: "('a->'b)->'a->'b"
|
| nipkow@243 | 17 |
|
| nipkow@243 | 18 |
rules |
| nipkow@243 | 19 |
|
| nipkow@243 | 20 |
inst_cfun_pcpo "UU::'a->'b = UU_cfun" |
| nipkow@243 | 21 |
|
| nipkow@243 | 22 |
Istrictify_def "Istrictify(f,x) == (@z.\ |
| nipkow@243 | 23 |
\ ( x=UU --> z = UU)\ |
| nipkow@243 | 24 |
\ & (~x=UU --> z = f[x]))" |
| nipkow@243 | 25 |
|
| nipkow@243 | 26 |
strictify_def "strictify == (LAM f x.Istrictify(f,x))" |
| nipkow@243 | 27 |
|
| nipkow@243 | 28 |
end |
| nipkow@243 | 29 |
|
| nipkow@243 | 30 |
|
| nipkow@243 | 31 |