1.1 --- a/doc-src/TutorialI/Advanced/simp.thy	Tue Jun 06 15:02:55 2006 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/simp.thy	Tue Jun 06 16:07:10 2006 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  Only the first argument is simplified; the others remain unchanged.
     1.5  This makes simplification much faster and is faithful to the evaluation
     1.6  strategy in programming languages, which is why this is the default
     1.7 -congruence rule for @{text if}. Analogous rules control the evaluation of
     1.8 +congruence rule for @{text "if"}. Analogous rules control the evaluation of
     1.9  @{text case} expressions.
    1.10  
    1.11  You can declare your own congruence rules with the attribute \attrdx{cong},
    1.12 @@ -170,7 +170,7 @@
    1.13  P \land Q &\mapsto& P,\ Q \nonumber\\
    1.14  \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
    1.15  \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
    1.16 -@{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
    1.17 +@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
    1.18   P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
    1.19  \end{eqnarray}
    1.20  Once this conversion process is finished, all remaining non-equations

     2.1 --- a/doc-src/TutorialI/Misc/simp.thy	Tue Jun 06 15:02:55 2006 +0200
     2.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Tue Jun 06 16:07:10 2006 +0200
     2.3 @@ -330,7 +330,7 @@
     2.4  text{*
     2.5  Polished proofs typically perform splitting within @{text simp} rather than 
     2.6  invoking the @{text split} method.  However, if a goal contains
     2.7 -several @{text if} and @{text case} expressions, 
     2.8 +several @{text "if"} and @{text case} expressions, 
     2.9  the @{text split} method can be
    2.10  helpful in selectively exploring the effects of splitting.
    2.11  

     3.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 15:02:55 2006 +0200
     3.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 16:07:10 2006 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  recursion equations become simplification rules, just as with
     3.5  \isacommand{primrec}. In most cases this works fine, but there is a subtle
     3.6  problem that must be mentioned: simplification may not
     3.7 -terminate because of automatic splitting of @{text if}.
     3.8 +terminate because of automatic splitting of @{text "if"}.
     3.9  \index{*if expressions!splitting of}
    3.10  Let us look at an example:
    3.11  *}
    3.12 @@ -26,7 +26,7 @@
    3.13  the recursive call inside the @{text else} branch, which is why programming
    3.14  languages and our simplifier don't do that. Unfortunately the simplifier does
    3.15  something else that leads to the same problem: it splits 
    3.16 -each @{text if}-expression unless its
    3.17 +each @{text "if"}-expression unless its
    3.18  condition simplifies to @{term True} or @{term False}.  For
    3.19  example, simplification reduces
    3.20  @{term[display]"gcd(m,n) = k"}
    3.21 @@ -35,7 +35,7 @@
    3.22  where the condition cannot be reduced further, and splitting leads to
    3.23  @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    3.24  Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    3.25 -an @{text if}, it is unfolded again, which leads to an infinite chain of
    3.26 +an @{text "if"}, it is unfolded again, which leads to an infinite chain of
    3.27  simplification steps. Fortunately, this problem can be avoided in many
    3.28  different ways.
    3.29  
    3.30 @@ -43,10 +43,10 @@
    3.31  @{thm[source]split_if},
    3.32  as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    3.33  approach: you will often have to invoke the rule explicitly when
    3.34 -@{text if} is involved.
    3.35 +@{text "if"} is involved.
    3.36  
    3.37  If possible, the definition should be given by pattern matching on the left
    3.38 -rather than @{text if} on the right. In the case of @{term gcd} the
    3.39 +rather than @{text "if"} on the right. In the case of @{term gcd} the
    3.40  following alternative definition suggests itself:
    3.41  *}
    3.42  
    3.43 @@ -61,7 +61,7 @@
    3.44  @{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
    3.45  may not be expressible by pattern matching.
    3.46  
    3.47 -A simple alternative is to replace @{text if} by @{text case}, 
    3.48 +A simple alternative is to replace @{text "if"} by @{text case}, 
    3.49  which is also available for @{typ bool} and is not split automatically:
    3.50  *}
    3.51  
    3.52 @@ -88,7 +88,7 @@
    3.53  
    3.54  text{*\noindent
    3.55  Simplification terminates for these proofs because the condition of the @{text
    3.56 -if} simplifies to @{term True} or @{term False}.
    3.57 +"if"} simplifies to @{term True} or @{term False}.
    3.58  Now we can disable the original simplification rule:
    3.59  *}
    3.60  

     4.1 --- a/doc-src/ZF/If.thy	Tue Jun 06 15:02:55 2006 +0200
     4.2 +++ b/doc-src/ZF/If.thy	Tue Jun 06 16:07:10 2006 +0200
     4.3 @@ -9,8 +9,8 @@
     4.4  theory If imports FOL begin
     4.5  
     4.6  constdefs
     4.7 -  if :: "[o,o,o]=>o"
     4.8 -   "if(P,Q,R) == P&Q | ~P&R"
     4.9 +  "if" :: "[o,o,o]=>o"
    4.10 +  "if(P,Q,R) == P&Q | ~P&R"
    4.11  
    4.12  lemma ifI:
    4.13      "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"