src/HOL/Bali/TypeSafe.thy

   proof (induct)
     case (Abrupt xc s t L accC T A) 
     from `(Some xc, s)\<Colon>\<preceq>(G,L)`
     show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
       (normal (Some xc, s) 
-      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
+      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and> 
       (error_free (Some xc, s) = error_free (Some xc, s))"
       by simp
   next
     case (Skip s L accC T A)
     from `Norm s\<Colon>\<preceq>(G, L)` and

    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
    and      wf: "wf_prog G" 
    and  abrupt: "\<And> s t abr L accC T A. 
                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
                    \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
-                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
+                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
    and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
    and    expr: "\<And> e s0 s1 v L accC eT E.
                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>
                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E;