diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -49,10 +49,10 @@
 
 text{*\noindent
 Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
-an \isa{if}, this leads to an infinite chain of simplification steps.
+an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
 Fortunately, this problem can be avoided in many different ways.
 
-Of course the most radical solution is to disable the offending
+The most radical solution is to disable the offending
 \isa{split_if} as shown in the section on case splits in
 \S\ref{sec:SimpFeatures}.
 However, we do not recommend this because it means you will often have to