diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Nov 07 18:38:24 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Nov 08 14:38:04 2000 +0100
@@ -60,8 +60,9 @@
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this is not a complete success:
-\begin{isabelle}\makeatother
-~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
 \end{isabelle}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed