# HG changeset patch
# User wenzelm
# Date 959166961 -7200
# Node ID 17365afd950249d9fc07e6bc6c28727b24029904
# Parent  96964d43a472de627ed90269d58733bb88dece7b
fixed index;

diff -r 96964d43a472 -r 17365afd9502 doc-src/IsarRef/hol.tex
--- 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}.