doc-src/IsarRef/hol.tex
changeset 9751 1287787744a7
parent 9695 ec7d7f877712
child 9800 221388d5696d
--- 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