diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Jul 16 13:14:19 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Jul 17 13:46:21 2001 +0200 @@ -50,7 +50,7 @@ In general, the format of invoking recursion induction is \begin{quote} \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} -\end{quote}\index{*induct_tac}% +\end{quote}\index{*induct_tac (method)}% where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the name of a function that takes an $n$-tuple. Usually the subgoal will contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The