added raw_term_sorts and changed typ_of_term accordingly (part of fix
of the typevar-sort-constraint BUG);
various minor internal changes;
(* Title: HOLCF/ssum3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ++ for class pcpo
*)
Ssum3 = Ssum2 +
arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
consts
sinl :: "'a -> ('a++'b)"
sinr :: "'b -> ('a++'b)"
when :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
rules
inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
sinl_def "sinl == (LAM x.Isinl(x))"
sinr_def "sinr == (LAM x.Isinr(x))"
when_def "when == (LAM f g s.Iwhen(f)(g)(s))"
end