src/HOLCF/ssum1.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 243 c22b85994e17
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

(*  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