src/HOLCF/Cfun3.thy
author regensbu
Thu, 29 Jun 1995 16:28:40 +0200
changeset 1168 74be52691d62
parent 1150 66512c9e6bd6
child 1479 21eb5e156d91
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported

(*  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