author | wenzelm |
Tue, 12 Jan 1999 12:29:50 +0100 | |
changeset 6085 | 3d8dcb09dbfb |
parent 3842 | b55686a7b22c |
child 12030 | 46d57d0290a2 |
permissions | -rw-r--r-- |
(* 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