src/HOL/Bali/Conform.thy

--- a/src/HOL/Bali/Conform.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/Conform.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -17,7 +17,7 @@
 \end{itemize}
 *}
 
-types	env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
 
 
 section "extension of global store"
@@ -102,7 +102,7 @@
 constdefs
 
   conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
-	   "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+           "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
 
 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: conf_def)
@@ -250,7 +250,7 @@
 done
 
 lemma lconf_init_vals [intro!]: 
-	" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
+        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
 apply (unfold lconf_def)
 apply force
 done
@@ -338,7 +338,7 @@
   by (simp add: wlconf_def)
 
 lemma wlconf_init_vals [intro!]: 
-	" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
+        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
 apply (unfold wlconf_def)
 apply force
 done
@@ -352,9 +352,9 @@
 constdefs
 
   oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool"  ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70)
-	   "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
+           "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
                            (case r of 
-		              Heap a \<Rightarrow> is_type G (obj_ty obj) 
+                              Heap a \<Rightarrow> is_type G (obj_ty obj) 
                             | Stat C \<Rightarrow> True)"
 
 
@@ -405,11 +405,11 @@
 by (auto simp: conforms_def Let_def)
 
 lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
-	  G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
+          G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
 by (auto simp: conforms_def Let_def)
 
 lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
-	  (locals s) Result \<noteq> None"
+          (locals s) Result \<noteq> None"
 by (auto simp: conforms_def Let_def)
 
 lemma conforms_RefTD: