src/HOLCF/Ssum2.thy

New function read_cterms is a combination of read_def_cterm and
read_cterm. It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg. More informative messages can
be printed this way.

(*  Title: 	HOLCF/ssum2.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Class Instance ++::(pcpo,pcpo)po
*)

Ssum2 = Ssum1 + 

arities "++" :: (pcpo,pcpo)po
(* Witness for the above arity axiom is ssum1.ML *)

rules

(* instance of << for type ['a ++ 'b]  *)

inst_ssum_po	"((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"

end