--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Apr 25 21:29:14 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Thu Apr 26 12:00:01 2007 +0200
@@ -55,8 +55,7 @@
\end{isabelle}
write
\begin{isabelle}%
-\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\isaindent{\ \ \ \ \ }{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
\end{isabelle}
Note that \isa{case}-expressions may need to be enclosed in parentheses to