--- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Aug 02 11:30:38 2000 +0200
@@ -1,20 +1,25 @@
\begin{isabelle}%
%
\begin{isamarkuptext}%
-We define a tail-recursive version of list-reversal,
-i.e.\ one that can be compiled into a loop:%
+Function \isa{rev} has quadratic worst-case running time
+because it calls function \isa{\at} for each element of the list and
+\isa{\at} is linear in its first argument. A linear time version of
+\isa{rev} reqires an extra argument where the result is accumulated
+gradually, using only \isa{\#}:%
\end{isamarkuptext}%
\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
\isacommand{primrec}\isanewline
{"}itrev~[]~~~~~ys~=~ys{"}\isanewline
{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
\begin{isamarkuptext}%
-\noindent
-The behaviour of \isa{itrev} is simple: it reverses its first argument by
-stacking its elements onto the second argument, and returning that second
-argument when the first one becomes empty.
-We need to show that \isa{itrev} does indeed reverse its first argument
-provided the second one is empty:%
+\noindent The behaviour of \isa{itrev} is simple: it reverses
+its first argument by stacking its elements onto the second argument,
+and returning that second argument when the first one becomes
+empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+compiled into a loop.
+
+Naturally, we would like to show that \isa{itrev} does indeed reverse
+its first argument provided the second one is empty:%
\end{isamarkuptext}%
\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
\begin{isamarkuptxt}%