--- 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