--- a/src/HOL/Bali/AxSem.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/AxSem.thy Sat Oct 17 14:43:18 2009 +0200
@@ -519,7 +519,7 @@
G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
| NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q}; G,A\<turnstile>{Q} e-\<succ>
- {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
+ {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
| Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..