src/HOLCF/ssum3.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     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