doc-src/TutorialI/Recdef/simplification.thy

--- a/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -7,7 +7,7 @@
 equations become simplification rules, just as with
 \isacommand{primrec}. In most cases this works fine, but there is a subtle
 problem that must be mentioned: simplification may not
-terminate because of automatic splitting of \isa{if}.
+terminate because of automatic splitting of @{name"if"}.
 Let us look at an example:
 *}
 
@@ -24,10 +24,10 @@
 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 @{name"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
+something else which leads to the same problem: it splits @{name"if"}s if the
+condition simplifies to neither @{term"True"} nor @{term"False"}. For
 example, simplification reduces
 \begin{quote}
 @{term[display]"gcd(m,n) = k"}
@@ -41,18 +41,17 @@
 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
 \end{quote}
 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of
+an @{name"if"}, it is unfolded again, which leads to an infinite chain of
 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 \@{name"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 @{name"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
+rather than @{name"if"} on the right. In the case of @{term"gcd"} the
 following alternative definition suggests itself:
 *}
 
@@ -64,11 +63,11 @@
 
 text{*\noindent
 Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+@{prop"n ~= 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
-is also available for \isa{bool} but is not split automatically:
+A very simple alternative is to replace @{name"if"} by @{name"case"}, which
+is also available for @{typ"bool"} but is not split automatically:
 *}
 
 consts gcd2 :: "nat*nat \\<Rightarrow> nat";
@@ -79,7 +78,7 @@
 In fact, this is probably the neatest solution next to pattern matching.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove
+derived conditional ones. For @{term"gcd"} it means we have to prove
 *}
 
 lemma [simp]: "gcd (m, 0) = m";