--- 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