src/HOLCF/Pcpo.thy
author nipkow
Mon, 10 Oct 1994 18:09:58 +0100
changeset 628 bb3f87f9cafe
parent 625 119391dd1d59
child 1274 ea0668a1c0ba
permissions -rw-r--r--
corrected problems with changed binding power of ::.

Pcpo = Porder +

classes pcpo < po
arities void :: pcpo

consts	
	UU :: "'a::pcpo"	
rules

minimal	"UU << x"	
cpo	"is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" 

inst_void_pcpo	"(UU::void) = UU_void"

end