src/HOLCF/Cprod2.thy
author wenzelm
Wed, 20 Feb 2002 00:53:53 +0100
changeset 12902 a23dc0b7566f
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
Symbol.bump_string;

(*  Title:      HOLCF/Cprod2.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Class Instance *::(pcpo,pcpo)po

*)

Cprod2 = Cprod1 + 

default pcpo

instance "*"::(cpo,cpo)po 
	(refl_less_cprod,antisym_less_cprod,trans_less_cprod)
end