src/HOL/Bali/Trans.thy
changeset 32960 69916a850301
parent 30952 7ab2716dd93b
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/Trans.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -124,11 +124,11 @@
     1.4      G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
     1.5   
     1.6    (* cf. 15.15 *)
     1.7 -| CastE:	
     1.8 +| CastE:
     1.9     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
    1.10      \<Longrightarrow>
    1.11      G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
    1.12 -| Cast:	
    1.13 +| Cast:
    1.14     "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
    1.15      \<Longrightarrow> 
    1.16      G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
    1.17 @@ -143,7 +143,7 @@
    1.18            G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
    1.19  
    1.20    (* cf. 15.7.1 *)
    1.21 -(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
    1.22 +(*Lit                           "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
    1.23  
    1.24  | UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
    1.25             \<Longrightarrow>