--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Jan 10 11:22:03 2002 +0100
@@ -189,7 +189,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}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} is trivial and we focus on
+distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
the other case:%
\end{isamarkuptxt}%
\isamarkuptrue%