1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 15:02:55 2006 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 16:07:10 2006 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  recursion 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 @{text if}.
     1.8 +terminate because of automatic splitting of @{text "if"}.
     1.9  \index{*if expressions!splitting of}
    1.10  Let us look at an example:
    1.11  *}
    1.12 @@ -26,7 +26,7 @@
    1.13  the recursive call inside the @{text else} branch, which is why programming
    1.14  languages and our simplifier don't do that. Unfortunately the simplifier does
    1.15  something else that leads to the same problem: it splits 
    1.16 -each @{text if}-expression unless its
    1.17 +each @{text "if"}-expression unless its
    1.18  condition simplifies to @{term True} or @{term False}.  For
    1.19  example, simplification reduces
    1.20  @{term[display]"gcd(m,n) = k"}
    1.21 @@ -35,7 +35,7 @@
    1.22  where the condition cannot be reduced further, and splitting leads to
    1.23  @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    1.24  Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    1.25 -an @{text if}, it is unfolded again, which leads to an infinite chain of
    1.26 +an @{text "if"}, it is unfolded again, which leads to an infinite chain of
    1.27  simplification steps. Fortunately, this problem can be avoided in many
    1.28  different ways.
    1.29  
    1.30 @@ -43,10 +43,10 @@
    1.31  @{thm[source]split_if},
    1.32  as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    1.33  approach: you will often have to invoke the rule explicitly when
    1.34 -@{text if} is involved.
    1.35 +@{text "if"} is involved.
    1.36  
    1.37  If possible, the definition should be given by pattern matching on the left
    1.38 -rather than @{text if} on the right. In the case of @{term gcd} the
    1.39 +rather than @{text "if"} on the right. In the case of @{term gcd} the
    1.40  following alternative definition suggests itself:
    1.41  *}
    1.42  
    1.43 @@ -61,7 +61,7 @@
    1.44  @{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
    1.45  may not be expressible by pattern matching.
    1.46  
    1.47 -A simple alternative is to replace @{text if} by @{text case}, 
    1.48 +A simple alternative is to replace @{text "if"} by @{text case}, 
    1.49  which is also available for @{typ bool} and is not split automatically:
    1.50  *}
    1.51  
    1.52 @@ -88,7 +88,7 @@
    1.53  
    1.54  text{*\noindent
    1.55  Simplification terminates for these proofs because the condition of the @{text
    1.56 -if} simplifies to @{term True} or @{term False}.
    1.57 +"if"} simplifies to @{term True} or @{term False}.
    1.58  Now we can disable the original simplification rule:
    1.59  *}
    1.60