src/HOL/Bali/TypeSafe.thy
changeset 19796 d86e7b1fc472
parent 18585 5d379fe2eb74
child 21765 89275a3ed7be
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Jun 06 19:24:05 2006 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Jun 06 20:42:25 2006 +0200
     1.3 @@ -3878,7 +3878,7 @@
     1.4                                 P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
     1.5                          \<rbrakk> \<Longrightarrow> Q 
     1.6                    \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
     1.7 -    and    if: "\<And> b c1 c2 e s0 s1 s2 L accC E.
     1.8 +    and  "if": "\<And> b c1 c2 e s0 s1 s2 L accC E.
     1.9                  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
    1.10                   G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
    1.11                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
    1.12 @@ -4030,7 +4030,7 @@
    1.13      }
    1.14      with eval_e eval_then_else wt_e wt_then_else da_e P_e
    1.15      show ?case
    1.16 -      by (rule if) iprover+
    1.17 +      by (rule "if") iprover+
    1.18    next
    1.19      oops
    1.20