src/HOLCF/Ssum1.thy

--- a/src/HOLCF/Ssum1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum1.thy	Sun May 25 11:07:52 1997 +0200
@@ -8,8 +8,10 @@
 
 Ssum1 = Ssum0 +
 
+instance "++"::(pcpo,pcpo)sq_ord
+
 defs
-  less_ssum_def "less == (%s1 s2.@z.
+  less_ssum_def "(op <<) == (%s1 s2.@z.
          (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
         &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
         &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))