--- a/src/HOLCF/Ssum3.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Ssum3.thy Thu Jun 29 16:28:40 1995 +0200
@@ -11,19 +11,19 @@
arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
consts
- sinl :: "'a -> ('a++'b)"
- sinr :: "'b -> ('a++'b)"
- when :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
+ sinl :: "'a -> ('a++'b)"
+ sinr :: "'b -> ('a++'b)"
+ sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
rules
inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
+
+defs
+
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))"
+sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
end
-
-
-