--- a/doc-src/TutorialI/Misc/Itrev.thy Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Nov 08 14:38:04 2000 +0100
@@ -61,9 +61,7 @@
txt{*\noindent
Unfortunately, this is not a complete success:
-\begin{isabelle}\makeatother
-~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
-\end{isabelle}
+@{subgoals[display,indent=0,margin=65]}
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed
@{term"[]"}. The corresponding heuristic: