--- 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