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