--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Fri Jan 12 16:07:20 2001 +0100
@@ -11,8 +11,9 @@
and closed with the observation that the associated schema for the definition
of primitive recursive functions leads to overly verbose definitions. Moreover,
if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
-you needed to reprove many lemmas reminiscent of similar lemmas about
-\isa{rev}. We will now show you how \isacommand{recdef} can simplify
+you needed to declare essentially the same function as \isa{rev}
+and prove many standard properties of list reverse all over again.
+We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
choose exercise~\ref{ex:trev-trev}:%
\end{isamarkuptext}%