src/HOLCF/Pcpo.thy
author clasohm
Wed, 13 Dec 1995 14:14:06 +0100
changeset 1403 cdfa3ffcead2
parent 1274 ea0668a1c0ba
child 1479 21eb5e156d91
permissions -rw-r--r--
renamed parents_of to parents_of_name to avoid name clash with function from thm.ML

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"

(* start 8bit 1 *)
(* end 8bit 1 *)
end