diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum1.thy --- 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