diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -59,12 +59,12 @@
 
 translations
 
-	"G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
-	"G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
-  	(* Defined in Decl.thy:
+        "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
+        "G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
+        (* Defined in Decl.thy:
         "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
-	"G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
-	*)
+        "G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
+        *)
         "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
 
 
@@ -202,12 +202,12 @@
       assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C"
       show "False"
       proof -
-	from subcls_D_C subcls1_C_Z
-	have "G\<turnstile>D \<prec>\<^sub>C Z"
-	  by (auto dest: r_into_trancl trancl_trans)
-	with nsubcls_D_Z
-	show ?thesis
-	  by (rule notE)
+        from subcls_D_C subcls1_C_Z
+        have "G\<turnstile>D \<prec>\<^sub>C Z"
+          by (auto dest: r_into_trancl trancl_trans)
+        with nsubcls_D_Z
+        show ?thesis
+          by (rule notE)
       qed
     qed
   qed  
@@ -243,16 +243,16 @@
       assume eq_C_D: "C=D"
       show "False"
       proof -
-	from subcls1_C_Z eq_C_D 
-	have "G\<turnstile>D \<prec>\<^sub>C Z"
-	  by (auto)
-	also
-	from subcls_Z_D ws   
-	have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
-	  by (rule subcls_acyclic)
-	ultimately 
-	show ?thesis 
-	  by - (rule notE)
+        from subcls1_C_Z eq_C_D 
+        have "G\<turnstile>D \<prec>\<^sub>C Z"
+          by (auto)
+        also
+        from subcls_Z_D ws   
+        have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
+          by (rule subcls_acyclic)
+        ultimately 
+        show ?thesis 
+          by - (rule notE)
       qed
     qed
   qed
@@ -298,12 +298,12 @@
       case Eq
       with ws subcls_C_D
       show ?thesis 
-	by (auto dest: subcls_irrefl)
+        by (auto dest: subcls_irrefl)
     next
       case Subcls
       with nsubcls_D_C
       show ?thesis
-	by blast
+        by blast
     qed
   qed
 qed
@@ -387,7 +387,7 @@
 
 inductive
  --{*widening, viz. method invocation conversion, cf. 5.3
-			    i.e. kind of syntactic subtyping *}
+                            i.e. kind of syntactic subtyping *}
   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   for G :: prog
 where
@@ -619,8 +619,8 @@
 | obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
 | int_cls: "G\<turnstile>     Iface I\<succ>Class C"
 | subint:  "imethds G I hidings imethds G J entails 
-	   (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
-	   \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
+           (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
+           \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
 | array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
 
 (*unused*)
@@ -637,7 +637,7 @@
 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
 
 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
-				  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
+                                  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
 
 text {*