src/HOLCF/lift3.thy
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 243 c22b85994e17
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.

(*  Title: 	HOLCF/lift3.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen


Class instance of  ('a)u for class pcpo

*)

Lift3 = Lift2 +

arities "u" :: (pcpo)pcpo			(* Witness lift2.ML *)

consts  
	up	     :: "'a -> ('a)u" 
	lift         :: "('a->'c)-> ('a)u -> 'c"

rules 

inst_lift_pcpo	"UU::('a)u = UU_lift"

up_def		"up     == (LAM x.Iup(x))"
lift_def	"lift   == (LAM f p.Ilift(f)(p))"

end