diff -r d1415164b814 -r 751fde5307e4 doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 28 09:32:51 2000 +0200
@@ -36,7 +36,7 @@
 \end{isabellepar}%
 The rest is pure simplification:%
 \end{isamarkuptxt}%
-\isacommand{by}\ auto%
+\isacommand{by}\ simp\_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
@@ -52,13 +52,13 @@
 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
 induction rules do not mention $f$ at all. For example \isa{sep.induct}
 \begin{isabellepar}%
-{\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline
-~~{\isasymAnd}a~x.~?P~a~[x];\isanewline
-~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}~?P~?u~?v%
+{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
+~~{\isasymAnd}a~x.~P~a~[x];\isanewline
+~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}~P~u~v%
 \end{isabellepar}%
-merely says that in order to prove a property \isa{?P} of \isa{?u} and
-\isa{?v} you need to prove it for the three cases where \isa{?v} is the
+merely says that in order to prove a property \isa{P} of \isa{u} and
+\isa{v} you need to prove it for the three cases where \isa{v} is the
 empty list, the singleton list, and the list with at least two elements
 (in which case you may assume it holds for the tail of that list).%
 \end{isamarkuptext}%