--- a/doc-src/Tutorial/fp.tex Wed Oct 13 15:18:15 1999 +0200
+++ b/doc-src/Tutorial/fp.tex Wed Oct 13 15:41:24 1999 +0200
@@ -1356,7 +1356,7 @@
theorems simultaneously:
\begin{quote}\small
\verbatiminput{Datatype/abgoalind.ML}
-\end{quote}\indexbold{*mutual_induct_tac}
+\end{quote}
The resulting 8 goals (one for each constructor) are proved in one fell swoop
\texttt{by Auto_tac;}.
@@ -1365,7 +1365,7 @@
\[ P@1(x@1)\ \texttt{\&}\ \dots\ \texttt{\&}\ P@n(x@n) \]
where each variable $x@i$ is of type $\tau@i$. Induction is started by
\begin{ttbox}
-by(mutual_induct_tac ["\(x@1\)",\(\dots\),"\(x@n\)"] \(k\));
+by(induct_tac "\(x@1\) \(\dots\) \(x@n\)" \(k\));
\end{ttbox}
\begin{exercise}