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