--- a/src/HOLCF/Cprod3.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Cprod3.thy Thu Jun 29 16:28:40 1995 +0200
@@ -18,18 +18,23 @@
csnd :: "('a*'b)->'b"
csplit :: "('a->'b->'c)->('a*'b)->'c"
-syntax "@cpair" :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
+syntax
+ "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
+
-translations "x#y" == "cpair[x][y]"
+translations
+ "<x, y, z>" == "<x, <y, z>>"
+ "<x, y>" == "cpair`x`y"
rules
-inst_cprod_pcpo "(UU::'a*'b) = <UU,UU>"
+inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
-cpair_def "cpair == (LAM x y.<x,y>)"
+defs
+cpair_def "cpair == (LAM x y.(x,y))"
cfst_def "cfst == (LAM p.fst(p))"
csnd_def "csnd == (LAM p.snd(p))"
-csplit_def "csplit == (LAM f p.f[cfst[p]][csnd[p]])"
+csplit_def "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
end