src/HOL/Bali/Trans.thy
changeset 28524 644b62cf678f
parent 23747 b07cff284683
child 30952 7ab2716dd93b
     1.1 --- a/src/HOL/Bali/Trans.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4                    \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
     1.5                    \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
     1.6                  \<Longrightarrow> 
     1.7 -                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
     1.8 +                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
     1.9  
    1.10  | InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
    1.11               \<Longrightarrow>