| changeset 2278 | d63ffafce255 |
| parent 1479 | 21eb5e156d91 |
| child 2291 | fbd14a05fb88 |
--- a/src/HOLCF/Ssum3.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Ssum3.thy Fri Nov 29 12:22:22 1996 +0100 @@ -30,6 +30,9 @@ "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s" (* start 8bit 1 *) +translations +"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(¤x.t1)`(¤y.t2)`s" + (* end 8bit 1 *) end