--- a/src/HOLCF/Sprod3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,7 +8,7 @@
Sprod3 = Sprod2 +
-arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
+instance "**" :: (pcpo,pcpo)pcpo (least_sprod,cpo_sprod)
consts
spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
@@ -17,18 +17,14 @@
ssplit :: "('a->'b->'c)->('a**'b)->'c"
syntax
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
+ "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
translations
"(|x, y, z|)" == "(|x, (|y, z|)|)"
"(|x, y|)" == "spair`x`y"
syntax (symbols)
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)")
-
-rules
-
-inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
+ "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)")
defs
spair_def "spair == (LAM x y.Ispair x y)"
@@ -36,7 +32,6 @@
ssnd_def "ssnd == (LAM p.Issnd p)"
ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
-
end