--- a/src/HOLCF/Ssum3.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Ssum3.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/ssum3.thy
+(* Title: HOLCF/ssum3.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ++ for class pcpo
@@ -8,23 +8,23 @@
Ssum3 = Ssum2 +
-arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
+arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
consts
- sinl :: "'a -> ('a++'b)"
- sinr :: "'b -> ('a++'b)"
- sswhen :: "('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)"
+inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
defs
-sinl_def "sinl == (LAM x.Isinl(x))"
-sinr_def "sinr == (LAM x.Isinr(x))"
-sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
+sinl_def "sinl == (LAM x.Isinl(x))"
+sinr_def "sinr == (LAM x.Isinr(x))"
+sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))"
translations
"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"