src/HOLCF/Lift3.thy
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 1168 74be52691d62
     1.1 --- a/src/HOLCF/Lift3.thy	Wed Jun 29 12:01:17 1994 +0200
     1.2 +++ b/src/HOLCF/Lift3.thy	Wed Jun 29 12:03:41 1994 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  rules 
     1.6  
     1.7 -inst_lift_pcpo	"UU::('a)u = UU_lift"
     1.8 +inst_lift_pcpo	"(UU::('a)u) = UU_lift"
     1.9  
    1.10  up_def		"up     == (LAM x.Iup(x))"
    1.11  lift_def	"lift   == (LAM f p.Ilift(f)(p))"