--- a/doc-src/TutorialI/Recdef/simplification.thy Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy Mon Mar 19 13:28:06 2001 +0100
@@ -37,11 +37,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending
-@{thm[source]split_if} as shown in the section on case splits in
-\S\ref{sec:Simplification}. However, we do not recommend this because it
-means you will often have to invoke the rule explicitly when @{text if} is
-involved.
+The most radical solution is to disable the offending @{thm[source]split_if}
+as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
+because it means you will often have to invoke the rule explicitly when
+@{text if} is involved.
If possible, the definition should be given by pattern matching on the left
rather than @{text if} on the right. In the case of @{term gcd} the