--- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 28 15:13:55 2000 +0200
@@ -36,7 +36,7 @@
\end{isabellepar}%
The rest is pure simplification:%
\end{isamarkuptxt}%
-\isacommand{by}\ simp\_all%
+\isacommand{by}\ simp{\isacharunderscore}all%
\begin{isamarkuptext}%
Try proving the above lemma by structural induction, and you find that you
need an additional case distinction. What is worse, the names of variables