--- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 28 15:13:55 2000 +0200
@@ -26,7 +26,7 @@
\noindent
There is no choice as to the induction variable, and we immediately simplify:%
\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
Unfortunately, this is not a complete success: