--- a/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 00:57:24 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 11:52:16 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
\isanewline
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
@@ -12,7 +13,7 @@
which is solved automatically:%
\end{isamarkuptxt}%
\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\end{isabelle}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"