--- a/doc-src/IsarRef/hol.tex Wed May 24 12:21:26 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Wed May 24 13:16:01 2000 +0200
@@ -113,8 +113,7 @@
syntax above has been slightly simplified over the old version, usually
requiring more quotes and less parentheses. Apart from proper proof methods
for case-analysis and induction, there are also emulations of ML tactics
-\texttt{case_tac}\indexisarmeth{case-tac} and
-\texttt{induct_tac}\indexisarmeth{induct-tac} available, see
+\texttt{case_tac} and \texttt{induct_tac} available, see
\S\ref{sec:induct_tac}.