# HG changeset patch
# User nipkow
# Date 783181255 -3600
# Node ID 2b16819fbd7188a27804c6f19b43e82420fc68b6
# Parent  ec05d2fdfeeeae280e05320a58163c00ea8dda41
simplified syntax of infix continuous functiuons

diff -r ec05d2fdfeee -r 2b16819fbd71 src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Tue Oct 25 13:16:49 1994 +0100
+++ b/src/HOLCF/Sprod3.thy	Wed Oct 26 15:20:55 1994 +0100
@@ -10,15 +10,14 @@
 
 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 *)
+consts
+	spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
 	sfst         :: "('a**'b)->'a"
 	ssnd         :: "('a**'b)->'b"
 	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
 
-translations "x##y" => "spair[x][y]"
+syntax	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
+translations "x##y" == "spair[x][y]"
 
 rules