src/HOLCF/Ssum3.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Ssum3.thy	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,29 @@
+(*  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
+
+
+