--- 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"
--- 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)"
--- 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 ()) *}
--- 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
--- 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
--- 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
--- 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
--- 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