src/HOLCF/Ssum1.thy

eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord

(*  Title:      HOLCF/Ssum1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen

Partial ordering for the strict sum ++
*)

Ssum1 = Ssum0 +

instance "++"::(pcpo,pcpo)sq_ord

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)))"

end