diff -r 499637e8f2c6 -r 0376cccd9118 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 11 10:44:42 2000 +0200
@@ -154,7 +154,7 @@
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{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}\ {\isadigit{0}}} is trivial and we focus on
 the other case:
 \begin{isabelle}
 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline