author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1479 | 21eb5e156d91 |
child 2640 | ee4dfce170a0 |
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 + arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *) consts Istrictify :: "('a->'b)=>'a=>'b" strictify :: "('a->'b)->'a->'b" rules inst_cfun_pcpo "(UU::'a->'b) = UU_cfun" defs Istrictify_def "Istrictify f x == if x=UU then UU else f`x" strictify_def "strictify == (LAM f x.Istrictify f x)" end