# HG changeset patch
# User wenzelm
# Date 1177581601 -7200
# Node ID 702542e7f88ce11e52dcc79ee6563b73e2f3a2ad
# Parent  d0f483fd57ddad7da08f2d9fffb7a61469e43115
updated;

diff -r d0f483fd57dd -r 702542e7f88c doc-src/TutorialI/Misc/document/case_exprs.tex
--- 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