diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/case_exprs.thy
--- 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:
 *}