src/HOLCF/Porder0.thy
changeset 442 13ac1fd0a14d
parent 298 3a0485439396
child 1274 ea0668a1c0ba
equal deleted inserted replaced
441:2b97bd6415b7 442:13ac1fd0a14d
    35 trans_less	"[|x<<y ; y<<z |] ==> x<<z"
    35 trans_less	"[|x<<y ; y<<z |] ==> x<<z"
    36 				(* witness trans_less_void   *)
    36 				(* witness trans_less_void   *)
    37 
    37 
    38 (* instance of << for the prototype void *)
    38 (* instance of << for the prototype void *)
    39 
    39 
    40 inst_void_po	"(op <<)::[void,void]=>bool = less_void"
    40 inst_void_po	"((op <<)::[void,void]=>bool) = less_void"
    41 
    41 
    42 end 
    42 end