src/HOLCF/Cprod2.thy
author paulson
Thu, 04 Dec 2003 10:29:17 +0100
changeset 14272 5efbb548107d
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
Tidying of the integer development; towards removing the abel_cancel simproc

(*  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