author | oheimb |
Mon, 16 Dec 1996 13:10:02 +0100 | |
changeset 2420 | cb21eef65704 |
parent 1479 | 21eb5e156d91 |
child 2640 | ee4dfce170a0 |
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 + consts less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool" rules less_ssum_def "less_ssum 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