diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -13,7 +13,7 @@
 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 declare essentially the same function as @{term"rev"}
-and prove many standard properties of list reverse all over again. 
+and prove many standard properties of list reversal 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}: