diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/document/Itrev.tex
--- 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}%