--- a/doc-src/IsarRef/hol.tex Wed Aug 30 17:54:26 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Wed Aug 30 17:54:46 2000 +0200
@@ -146,7 +146,7 @@
functions (using the TFL package).
\end{descr}
-Both definitions accommodate reasoning proof by induction (cf.\
+Both definitions accommodate reasoning by induction (cf.\
\S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
of the function definition) refers to a specific induction rule, with
parameters named according to the user-specified equations. Case names of