--- a/src/HOLCF/Cprod3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,16 +1,15 @@
-(* Title: HOLCF/cprod3.thy
+(* Title: HOLCF/Cprod3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-
Class instance of * for class pcpo
*)
Cprod3 = Cprod2 +
-arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *)
+instance "*" :: (pcpo,pcpo)pcpo (least_cprod,cpo_cprod)
consts
cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
@@ -21,15 +20,10 @@
syntax
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
-
translations
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "cpair`x`y"
-rules
-
-inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
-
defs
cpair_def "cpair == (LAM x y.(x,y))"
cfst_def "cfst == (LAM p.fst(p))"
@@ -70,7 +64,6 @@
(* Misc Definitions *)
CLet_def "CLet == LAM s. LAM f.f`s"
-
syntax
(* syntax for LAM <x,y,z>.E *)
"@Cpttrn" :: "[pttrn,pttrns] => pttrn" ("<_,/_>")