# HG changeset patch
# User wenzelm
# Date 1149619345 -7200
# Node ID d86e7b1fc472f186ccf608cf5b8020540ea1a0af
# Parent  746274ca400bf6b8f2d60289d676343d1be54fb2
quoted "if";

diff -r 746274ca400b -r d86e7b1fc472 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/CCL/Term.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -14,7 +14,7 @@
 
   one        :: "i"
 
-  if         :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
+  "if"       :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
 
   inl        :: "i=>i"
   inr        :: "i=>i"
diff -r 746274ca400b -r d86e7b1fc472 src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/FOL/ex/If.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -9,8 +9,8 @@
 theory If imports FOL begin
 
 constdefs
-  if :: "[o,o,o]=>o"
-   "if(P,Q,R) == P&Q | ~P&R"
+  "if" :: "[o,o,o]=>o"
+  "if(P,Q,R) == P&Q | ~P&R"
 
 lemma ifI:
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
diff -r 746274ca400b -r d86e7b1fc472 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/FOLP/ex/If.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -5,7 +5,7 @@
 begin
 
 constdefs
-  if :: "[o,o,o]=>o"
+  "if" :: "[o,o,o]=>o"
   "if(P,Q,R) == P&Q | ~P&R"
 
 ML {* use_legacy_bindings (the_context ()) *}
diff -r 746274ca400b -r d86e7b1fc472 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -3878,7 +3878,7 @@
                                P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
                         \<rbrakk> \<Longrightarrow> Q 
                   \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
-    and    if: "\<And> b c1 c2 e s0 s1 s2 L accC E.
+    and  "if": "\<And> b c1 c2 e s0 s1 s2 L accC E.
                 \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
                  G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
@@ -4030,7 +4030,7 @@
     }
     with eval_e eval_then_else wt_e wt_then_else da_e P_e
     show ?case
-      by (rule if) iprover+
+      by (rule "if") iprover+
   next
     oops
 
diff -r 746274ca400b -r d86e7b1fc472 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -1124,11 +1124,11 @@
 by (simplesubst split_if, blast)
 
 lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
-  -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
+  -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
   by (rule split_if)
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
-  -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
+  -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
   apply (simplesubst split_if, blast)
   done
 
diff -r 746274ca400b -r d86e7b1fc472 src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/HOL/IMP/Natural.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -165,7 +165,7 @@
   }
   moreover
   -- "now the other direction:"
-  { fix s s' assume if: "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
+  { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
     -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
     -- "of the @{text \<IF>} is executed, and both statements do nothing:"
     hence "\<not>b s \<Longrightarrow> s = s'" by simp
@@ -174,7 +174,7 @@
     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
     -- {* then this time only the @{text IfTrue} rule can have be used *}
     { assume b: "b s"
-      with if have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
+      with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
       -- "and for this, only the Semi-rule is applicable:"
       then obtain s'' where
         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
diff -r 746274ca400b -r d86e7b1fc472 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/ZF/IMP/Com.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -78,7 +78,7 @@
   | assignment ("x \<in> loc", "a \<in> aexp")       (infixl "\<ASSN>" 60)
   | semicolon ("c0 \<in> com", "c1 \<in> com")       ("_\<SEQ> _"  [60, 60] 10)
   | while ("b \<in> bexp", "c \<in> com")            ("\<WHILE> _ \<DO> _"  60)
-  | if ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
+  | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
 
 
 consts evalc :: i
diff -r 746274ca400b -r d86e7b1fc472 src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/ZF/IMP/Equiv.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -69,7 +69,7 @@
    apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
    apply (unfold Gamma_def)
    apply force
-  txt {* @{text if} *}
+  txt {* @{text "if"} *}
   apply auto
   done