diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -26,7 +26,7 @@
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
+the recursive call inside the \isa{if} branch, which is why programming
 languages and our simplifier don't do that. Unfortunately the simplifier does
 something else which leads to the same problem: it splits \isa{if}s if the
 condition simplifies to neither \isa{True} nor \isa{False}. For
@@ -59,11 +59,10 @@
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
 
-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
-invoke the rule explicitly when \isa{if} is involved.
+The most radical solution is to disable the offending \\isa{split{\isacharunderscore}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 \isa{if} is involved.
 
 If possible, the definition should be given by pattern matching on the left
 rather than \isa{if} on the right. In the case of \isa{gcd} the
@@ -76,7 +75,7 @@
 \begin{isamarkuptext}%
 \noindent
 Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+\isa{\mbox{n}\ {\isasymnoteq}\ \isadigit{0}}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A very simple alternative is to replace \isa{if} by \isa{case}, which