src/HOLCF/Ssum3.thy

--- a/src/HOLCF/Ssum3.thy	Fri Oct 06 16:17:08 1995 +0100
+++ b/src/HOLCF/Ssum3.thy	Fri Oct 06 17:25:24 1995 +0100
@@ -26,4 +26,10 @@
 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"
+
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
 end