diff -r 6c45813c2db1 -r d27253c4594f doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Oct 08 12:27:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Oct 08 12:28:43 2001 +0200
@@ -171,7 +171,7 @@
 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
 \end{isabelle}
 After stripping the \isa{{\isasymforall}i}, the proof continues with a case
-distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
+distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} is trivial and we focus on
 the other case:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline