
diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Feb 20 10:37:12 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




