--- a/src/HOLCF/Ssum1.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum1.thy Fri Oct 10 19:02:28 1997 +0200
@@ -12,10 +12,10 @@
defs
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))
- &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+ (! 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))
+ &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
end