src/HOLCF/Ssum2.thy
author clasohm
Wed, 21 Jun 1995 15:14:58 +0200
changeset 1150 66512c9e6bd6
parent 442 13ac1fd0a14d
child 1479 21eb5e156d91
permissions -rw-r--r--
removed \...\ inside strings

(*  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