src/HOL/Bali/TypeSafe.thy
changeset 28524 644b62cf678f
parent 24783 5a3e336a2e37
child 32693 6c6b1ba5e71e
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -1738,7 +1738,7 @@
     1.4      from `(Some xc, s)\<Colon>\<preceq>(G,L)`
     1.5      show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
     1.6        (normal (Some xc, s) 
     1.7 -      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
     1.8 +      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and> 
     1.9        (error_free (Some xc, s) = error_free (Some xc, s))"
    1.10        by simp
    1.11    next
    1.12 @@ -3850,7 +3850,7 @@
    1.13     and  abrupt: "\<And> s t abr L accC T A. 
    1.14                    \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
    1.15                     \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
    1.16 -                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
    1.17 +                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
    1.18     and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
    1.19     and    expr: "\<And> e s0 s1 v L accC eT E.
    1.20                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;