diff -r 72a76580ed2f -r 6e6c8d1ec89e doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Thu Feb 01 20:45:54 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Thu Feb 01 20:48:58 2001 +0100 @@ -49,7 +49,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}} +\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}% 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