| changeset 10834 | a7897aebbffc |
| parent 5439 | 2e0c18eedfd0 |
| child 12030 | 46d57d0290a2 |
--- a/src/HOLCF/Ssum3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Ssum3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -22,6 +22,6 @@ sscase_def "sscase == (LAM f g s. Iwhen(f)(g)(s))" translations -"case s of sinl`x => t1 | sinr`y => t2" == "sscase`(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