src/HOLCF/ssum3.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/ssum3.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Class instance of  ++ for class pcpo
     7 *)
     8 
     9 Ssum3 = Ssum2 +
    10 
    11 arities "++" :: (pcpo,pcpo)pcpo			(* Witness ssum2.ML *)
    12 
    13 consts  
    14 	sinl	     :: "'a -> ('a++'b)" 
    15 	sinr	     :: "'b -> ('a++'b)" 
    16 	when         :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
    17 
    18 rules 
    19 
    20 inst_ssum_pcpo	"UU::'a++'b = Isinl(UU)"
    21 
    22 sinl_def	"sinl   == (LAM x.Isinl(x))"
    23 sinr_def	"sinr   == (LAM x.Isinr(x))"
    24 when_def	"when   == (LAM f g s.Iwhen(f)(g)(s))"
    25 
    26 end
    27 
    28 
    29