changeset 3323 | 194ae2e0c193 |
parent 2640 | ee4dfce170a0 |
child 3842 | b55686a7b22c |
--- 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))