--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 18 18:30:19 2002 +0100
@@ -80,8 +80,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
@@ -264,7 +263,7 @@
the induction hypothesis:
*};
apply(blast);
-by(blast elim:less_SucE)
+by(blast elim: less_SucE)
text{*\noindent
The elimination rule @{thm[source]less_SucE} expresses the case distinction: