src/HOLCF/Cprod2.thy
changeset 2640 ee4dfce170a0
parent 1479 21eb5e156d91
child 2840 7e03e61612b0
     1.1 --- a/src/HOLCF/Cprod2.thy	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/Cprod2.thy	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOLCF/cprod2.thy
     1.5 +(*  Title:      HOLCF/Cprod2.thy
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8      Copyright   1993 Technische Universitaet Muenchen
     1.9 @@ -9,16 +9,8 @@
    1.10  
    1.11  Cprod2 = Cprod1 + 
    1.12  
    1.13 -(* Witness for the above arity axiom is cprod1.ML *)
    1.14 -
    1.15 -arities "*" :: (pcpo,pcpo)po
    1.16 -
    1.17 -rules
    1.18 -
    1.19 -(* instance of << for type ['a * 'b]  *)
    1.20 -
    1.21 -inst_cprod_po   "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
    1.22 -
    1.23 +instance "*"::(pcpo,pcpo)po 
    1.24 +	(refl_less_cprod,antisym_less_cprod,trans_less_cprod)
    1.25  end
    1.26  
    1.27