src/HOLCF/Sprod3.thy

--- a/src/HOLCF/Sprod3.thy	Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Sprod3.thy	Mon Dec 02 12:37:15 1996 +0100
@@ -34,12 +34,6 @@
 ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
 
 (* start 8bit 1 *)
-syntax  
-	"@Gstuple"    :: "['a, args] => 'a ** 'b"	("(1É_,/ _Ê)")
-
-translations
-	"Éx, y, zÊ"   == "Éx, Éy, zÊÊ"
-	"Éx, yÊ"      == "(|x,y|)"
 (* end 8bit 1 *)
 
 end