src/HOLCF/Cprod2.thy
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 2840 7e03e61612b0
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/Cprod2.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Class Instance *::(pcpo,pcpo)po
     7 
     8 *)
     9 
    10 Cprod2 = Cprod1 + 
    11 
    12 default pcpo
    13 
    14 instance "*"::(cpo,cpo)po 
    15 	(refl_less_cprod,antisym_less_cprod,trans_less_cprod)
    16 end
    17 
    18 
    19