diff -r 2995639c6a09 -r 90695f46440b doc-src/TutorialI/Recdef/Nested0.thy
--- 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}:
 *}