1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:05:20 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Aug 30 18:09:20 2000 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  equations become simplification rules, just as with
     1.5  \isacommand{primrec}. In most cases this works fine, but there is a subtle
     1.6  problem that must be mentioned: simplification may not
     1.7 -terminate because of automatic splitting of \isa{if}.
     1.8 +terminate because of automatic splitting of @{name"if"}.
     1.9  Let us look at an example:
    1.10  *}
    1.11  
    1.12 @@ -24,10 +24,10 @@
    1.13  is provded automatically because it is already present as a lemma in the
    1.14  arithmetic library. Thus the recursion equation becomes a simplification
    1.15  rule. Of course the equation is nonterminating if we are allowed to unfold
    1.16 -the recursive call inside the \isa{else} branch, which is why programming
    1.17 +the recursive call inside the @{name"if"} branch, which is why programming
    1.18  languages and our simplifier don't do that. Unfortunately the simplifier does
    1.19 -something else which leads to the same problem: it splits \isa{if}s if the
    1.20 -condition simplifies to neither \isa{True} nor \isa{False}. For
    1.21 +something else which leads to the same problem: it splits @{name"if"}s if the
    1.22 +condition simplifies to neither @{term"True"} nor @{term"False"}. For
    1.23  example, simplification reduces
    1.24  \begin{quote}
    1.25  @{term[display]"gcd(m,n) = k"}
    1.26 @@ -41,18 +41,17 @@
    1.27  @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    1.28  \end{quote}
    1.29  Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    1.30 -an \isa{if}, it is unfolded again, which leads to an infinite chain of
    1.31 +an @{name"if"}, it is unfolded again, which leads to an infinite chain of
    1.32  simplification steps. Fortunately, this problem can be avoided in many
    1.33  different ways.
    1.34  
    1.35 -The most radical solution is to disable the offending
    1.36 -\isa{split_if} as shown in the section on case splits in
    1.37 -\S\ref{sec:SimpFeatures}.
    1.38 -However, we do not recommend this because it means you will often have to
    1.39 -invoke the rule explicitly when \isa{if} is involved.
    1.40 +The most radical solution is to disable the offending \@{name"split_if"} as
    1.41 +shown in the section on case splits in \S\ref{sec:Simplification}.  However,
    1.42 +we do not recommend this because it means you will often have to invoke the
    1.43 +rule explicitly when @{name"if"} is involved.
    1.44  
    1.45  If possible, the definition should be given by pattern matching on the left
    1.46 -rather than \isa{if} on the right. In the case of \isa{gcd} the
    1.47 +rather than @{name"if"} on the right. In the case of @{term"gcd"} the
    1.48  following alternative definition suggests itself:
    1.49  *}
    1.50  
    1.51 @@ -64,11 +63,11 @@
    1.52  
    1.53  text{*\noindent
    1.54  Note that the order of equations is important and hides the side condition
    1.55 -\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
    1.56 +@{prop"n ~= 0"}. Unfortunately, in general the case distinction
    1.57  may not be expressible by pattern matching.
    1.58  
    1.59 -A very simple alternative is to replace \isa{if} by \isa{case}, which
    1.60 -is also available for \isa{bool} but is not split automatically:
    1.61 +A very simple alternative is to replace @{name"if"} by @{name"case"}, which
    1.62 +is also available for @{typ"bool"} but is not split automatically:
    1.63  *}
    1.64  
    1.65  consts gcd2 :: "nat*nat \\<Rightarrow> nat";
    1.66 @@ -79,7 +78,7 @@
    1.67  In fact, this is probably the neatest solution next to pattern matching.
    1.68  
    1.69  A final alternative is to replace the offending simplification rules by
    1.70 -derived conditional ones. For \isa{gcd} it means we have to prove
    1.71 +derived conditional ones. For @{term"gcd"} it means we have to prove
    1.72  *}
    1.73  
    1.74  lemma [simp]: "gcd (m, 0) = m";