diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -92,8 +92,7 @@
 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
 \end{equation}
 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
-Now you can perform
-perform induction on~$x$. An example appears in
+Now you can perform induction on~$x$. An example appears in
 \S\ref{sec:complete-ind} below.
 
 The very same problem may occur in connection with rule induction. Remember
@@ -309,7 +308,7 @@
 \ \isamarkuptrue%
 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent