changeset 2840 | 7e03e61612b0 |
parent 2640 | ee4dfce170a0 |
child 3693 | 37aa547fb564 |
--- a/src/HOLCF/Cprod3.thy Tue Mar 25 11:19:09 1997 +0100 +++ b/src/HOLCF/Cprod3.thy Wed Mar 26 13:44:05 1997 +0100 @@ -9,7 +9,8 @@ Cprod3 = Cprod2 + -instance "*" :: (pcpo,pcpo)pcpo (least_cprod,cpo_cprod) +instance "*" :: (cpo,cpo)cpo (cpo_cprod) +instance "*" :: (pcpo,pcpo)pcpo (least_cprod) consts cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)