diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -286,7 +286,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
 *}
@@ -324,7 +326,7 @@
 
 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*
 \noindent
@@ -335,7 +337,7 @@
 
 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 and then solve our main theorem:
@@ -343,7 +345,7 @@
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 apply(induct_tac xs);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 The final \isa{end} tells Isabelle to close the current theory because