--- a/doc-src/TutorialI/Recdef/Nested0.thy Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Fri Jan 12 16:32:01 2001 +0100
@@ -12,8 +12,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
-@{term"rev"}. We will now show you how \isacommand{recdef} can simplify
+you needed to declare essentially the same function as @{term"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}:
*}