src/HOLCF/ssum1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/ssum1.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Partial ordering for the strict sum ++
     7 *)
     8 
     9 Ssum1 = Ssum0 +
    10 
    11 consts
    12 
    13   less_ssum	:: "[('a ++ 'b),('a ++ 'b)] => bool"	
    14 
    15 rules
    16 
    17   less_ssum_def "less_ssum(s1,s2) == (@z.\
    18 \	 (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))\
    19 \	&(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))\
    20 \	&(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))\
    21 \	&(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
    22 
    23 end
    24 
    25