diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -265,7 +265,9 @@
 just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
 printed out after the final dot) the free variable \isa{xs} has been
 replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}.
+\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+followed by a dot, you can simply write \isacommand{by}\indexbold{by},
+which we do most of the time.
 
 Going back to the proof of the first lemma%
 \end{isamarkuptext}%
@@ -299,7 +301,7 @@
 \end{comment}
 \isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 succeeds without further ado.
@@ -308,14 +310,14 @@
 \end{isamarkuptext}%
 \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 and then solve our main theorem:%
 \end{isamarkuptext}%
 \isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline
 \isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 The final \isa{end} tells Isabelle to close the current theory because