diff -r c20f78a9606f -r c6b197ccf1f1 doc-src/TutorialI/Recdef/Induction.thy
--- a/doc-src/TutorialI/Recdef/Induction.thy	Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Oct 31 08:53:12 2000 +0100
@@ -31,13 +31,7 @@
 txt{*\noindent
 The resulting proof state has three subgoals corresponding to the three
 clauses for @{term"sep"}:
-\begin{isabelle}
-~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
-~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
-~3.~{\isasymAnd}a~x~y~zs.\isanewline
-~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
-~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
-\end{isabelle}
+@{subgoals[display,indent=0]}
 The rest is pure simplification:
 *}