author | slotosch |
Tue, 25 Mar 1997 11:13:12 +0100 | |
changeset 2838 | 2e908f29bc3d |
parent 2640 | ee4dfce170a0 |
child 3327 | 9b8e638f8602 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Cfun3.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class instance of -> for class pcpo *) Cfun3 = Cfun2 + instance "->" :: (cpo,cpo)cpo (cpo_cfun) instance "->" :: (cpo,pcpo)pcpo (least_cfun) default pcpo consts Istrictify :: "('a->'b)=>'a=>'b" strictify :: "('a->'b)->'a->'b" defs Istrictify_def "Istrictify f x == if x=UU then UU else f`x" strictify_def "strictify == (LAM f x.Istrictify f x)" end