1.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Tue Feb 20 10:18:26 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Feb 20 10:37:12 2001 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  
     1.5  In general, the format of invoking recursion induction is
     1.6  \begin{quote}
     1.7 -\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
     1.8 +\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
     1.9  \end{quote}\index{*induct_tac}%
    1.10  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
    1.11  name of a function that takes an $n$-tuple. Usually the subgoal will