--- a/src/HOLCF/Ssum3.thy Wed Sep 09 16:13:35 1998 +0200
+++ b/src/HOLCF/Ssum3.thy Wed Sep 09 16:21:08 1998 +0200
@@ -13,15 +13,15 @@
consts
sinl :: "'a -> ('a++'b)"
sinr :: "'b -> ('a++'b)"
- sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
+ sscase :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
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))"
+sscase_def "sscase == (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"
+"case s of sinl`x => t1 | sinr`y => t2" == "sscase`(LAM x. t1)`(LAM y. t2)`s"
end