diff -r c5fc121c2067 -r f0740137a65d doc-src/TutorialI/Misc/document/Itrev.tex
--- 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: