--- a/doc-src/TutorialI/Misc/document/cases.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
\isanewline
-\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
-\isacommand{apply}(case\_tac~xs)%
+\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline
+\isacommand{apply}(case\_tac\ xs)%
\begin{isamarkuptxt}%
\noindent
results in the proof state