src/HOL/Bali/AxSem.thy
changeset 32960 69916a850301
parent 28524 644b62cf678f
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -519,7 +519,7 @@
     1.4                                   G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
     1.5  
     1.6  | NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
     1.7 -	  {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
     1.8 +          {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
     1.9                                   G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
    1.10  
    1.11  | Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..