src/HOLCF/Lift3.thy
author clasohm
Wed Jun 29 12:03:41 1994 +0200 (1994-06-29)
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 1168 74be52691d62
permissions -rw-r--r--
added parentheses made necessary by change of constrain's precedence
     1 (*  Title: 	HOLCF/lift3.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 
     7 Class instance of  ('a)u for class pcpo
     8 
     9 *)
    10 
    11 Lift3 = Lift2 +
    12 
    13 arities "u" :: (pcpo)pcpo			(* Witness lift2.ML *)
    14 
    15 consts  
    16 	up	     :: "'a -> ('a)u" 
    17 	lift         :: "('a->'c)-> ('a)u -> 'c"
    18 
    19 rules 
    20 
    21 inst_lift_pcpo	"(UU::('a)u) = UU_lift"
    22 
    23 up_def		"up     == (LAM x.Iup(x))"
    24 lift_def	"lift   == (LAM f p.Ilift(f)(p))"
    25 
    26 end
    27 
    28 
    29