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