src/HOLCF/lift3.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     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