diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Jul 17 13:46:21 2001 +0200
@@ -225,12 +225,12 @@
 identity function.
 \end{exercise}
 
-Method \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
+Method \methdx{induct_tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}\index{*induct_tac}%
+\end{quote}
 where $y@1, \dots, y@n$ are variables in the first subgoal.
 The conclusion of $r$ can even be an (iterated) conjunction of formulae of
 the above form in which case the application is