# HG changeset patch
# User berghofe
# Date 939822084 -7200
# Node ID 6ddcc24038e183f5c35381235ce7682d1750c0ac
# Parent  5a3fa0c4b21521bb87d4d389a7c9c7b78682a87f
Eliminated mutual_induct_tac.

diff -r 5a3fa0c4b215 -r 6ddcc24038e1 doc-src/Tutorial/Datatype/abgoalfind.ML
--- a/doc-src/Tutorial/Datatype/abgoalfind.ML	Wed Oct 13 15:18:15 1999 +0200
+++ b/doc-src/Tutorial/Datatype/abgoalfind.ML	Wed Oct 13 15:41:24 1999 +0200
@@ -1,4 +1,4 @@
 Goal
  "evala env (substa s a) = evala (%x. evala env (s x)) a & \
 \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
-by(mutual_induct_tac ["a","b"] 1);
+by(induct_tac "a b" 1);
diff -r 5a3fa0c4b215 -r 6ddcc24038e1 doc-src/Tutorial/Datatype/abgoalind.ML
--- a/doc-src/Tutorial/Datatype/abgoalind.ML	Wed Oct 13 15:18:15 1999 +0200
+++ b/doc-src/Tutorial/Datatype/abgoalind.ML	Wed Oct 13 15:41:24 1999 +0200
@@ -1,4 +1,4 @@
 Goal
  "evala env (substa s a) = evala (%x. evala env (s x)) a & \
 \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
-by(mutual_induct_tac ["a","b"] 1);
+by(induct_tac "a b" 1);
diff -r 5a3fa0c4b215 -r 6ddcc24038e1 doc-src/Tutorial/Datatype/tidproof.ML
--- a/doc-src/Tutorial/Datatype/tidproof.ML	Wed Oct 13 15:18:15 1999 +0200
+++ b/doc-src/Tutorial/Datatype/tidproof.ML	Wed Oct 13 15:41:24 1999 +0200
@@ -1,4 +1,4 @@
 Goal "subst  Var t  = (t ::('a,'b)term)  & \
 \     substs Var ts = (ts::('a,'b)term list)";
-by(mutual_induct_tac ["t", "ts"] 1);
+by(induct_tac "t ts" 1);
 by(Auto_tac);
diff -r 5a3fa0c4b215 -r 6ddcc24038e1 doc-src/Tutorial/fp.tex
--- 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}