src/HOLCF/Pcpo.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1479 21eb5e156d91
child 2278 d63ffafce255
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.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