src/HOLCF/Pcpo.thy
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 625 119391dd1d59
--- a/src/HOLCF/Pcpo.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -28,12 +28,12 @@
 
 minimal		"UU << x"			(* witness is minimal_void *)
 
-cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
+cpo		"is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))" 
 						(* witness is cpo_void     *)
 						(* needs explicit type     *)
 
 (* instance of UU for the prototype void *)
 
-inst_void_pcpo	"UU::void = UU_void"
+inst_void_pcpo	"(UU::void) = UU_void"
 
 end