--- a/doc-src/TutorialI/Misc/case_exprs.thy Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/case_exprs.thy Wed Nov 08 14:38:04 2000 +0100
@@ -58,10 +58,7 @@
txt{*\noindent
results in the proof state
-\begin{isabelle}
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
which is solved automatically:
*}