--- a/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Feb 20 10:37:12 2001 +0100
@@ -47,7 +47,7 @@
In general, the format of invoking recursion induction is
\begin{quote}
-\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
+\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
\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