--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/sprod3.thy Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,39 @@
+(* Title: HOLCF/sprod3.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Class instance of ** for class pcpo
+*)
+
+Sprod3 = Sprod2 +
+
+arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
+
+consts
+ "@spair" :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
+ "cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair")
+ (* continuous strict pairing *)
+ sfst :: "('a**'b)->'a"
+ ssnd :: "('a**'b)->'b"
+ ssplit :: "('a->'b->'c)->('a**'b)->'c"
+
+rules
+
+inst_sprod_pcpo "UU::'a**'b = Ispair(UU,UU)"
+spair_def "spair == (LAM x y.Ispair(x,y))"
+sfst_def "sfst == (LAM p.Isfst(p))"
+ssnd_def "ssnd == (LAM p.Issnd(p))"
+ssplit_def "ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])"
+
+end
+
+ML
+
+(* ----------------------------------------------------------------------*)
+(* parse translations for the above mixfix *)
+(* ----------------------------------------------------------------------*)
+
+val parse_translation = [("@spair",mk_cinfixtr "@spair")];
+
+