--- a/src/HOLCF/Ssum0.thy Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Ssum0.thy Mon Dec 02 12:37:15 1996 +0100
@@ -52,14 +52,6 @@
&(!b. b~=UU & s=Isinr(b) --> z=g`b)"
(* start 8bit 1 *)
-types
-
-('a, 'b) "ó" (infixr 10)
-
-translations
-
-(type) "x ó y" == (type) "x ++ y"
-
(* end 8bit 1 *)
end