doc-src/TutorialI/Misc/AdvancedInd.thy

 as
 \begin{equation}\label{eqn:ind-over-term}
 \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
 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
 some inductively defined set and the $x@i$ are variables.  If instead we have

 Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
 hypothesis and case @{prop"m = n"} follows from the assumption, again using
 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:
 @{thm[display]"less_SucE"[no_vars]}