diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/Trans.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -124,11 +124,11 @@
     G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
  
   (* cf. 15.15 *)
-| CastE:	
+| CastE:
    "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
     \<Longrightarrow>
     G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
-| Cast:	
+| Cast:
    "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
     \<Longrightarrow> 
     G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
@@ -143,7 +143,7 @@
           G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
 
   (* cf. 15.7.1 *)
-(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
+(*Lit                           "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
 
 | UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
            \<Longrightarrow>