# HG changeset patch
# User wenzelm
# Date 967650886 -7200
# Node ID 1287787744a79b06eeef4aad6c4f37e9fee21822
# Parent  270cd9831e7bf512718c2bac7e53802e432a32ce
tuned;

diff -r 270cd9831e7b -r 1287787744a7 doc-src/IsarRef/hol.tex
--- 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