src/HOL/MicroJava/Comp/LemmasComp.thy

 (*  Title:      HOL/MicroJava/Comp/LemmasComp.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
 (* Lemmas for compiler correctness proof *)
 

 
     have fst_set: "(fst a \<in> fst ` set list) = (fst (f a) \<in> fst ` f ` set list)" 
     proof 
       assume as: "fst a \<in> fst ` set list" 
       then obtain x where fst_a_x: "x\<in>set list \<and> fst a = fst x" 
-	by (auto simp add: image_iff)
+        by (auto simp add: image_iff)
       then have "fst (f a) = fst (f x)" by (simp add: fst_eq)
       with as show "(fst (f a) \<in> fst ` f ` set list)" by (simp add: fst_a_x)
     next
       assume as: "fst (f a) \<in> fst ` f ` set list"
       then obtain x where fst_a_x: "x\<in>set list \<and> fst (f a) = fst (f x)"
-	by (auto simp add: image_iff)
+        by (auto simp add: image_iff)
       then have "fst a = fst x" by (simp add: fst_eq)
       with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x)
     qed
 
     with fst_eq Cons 

 apply (rule trans)
 
 apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
   g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" 
   in map_of_map_fst)
-defer				(* inj \<dots> *)
+defer                           (* inj \<dots> *)
 apply (simp add: inj_on_def split_beta) 
 apply (simp add: split_beta compMethod_def)
 apply (simp add: map_of_map [THEN sym])
 apply (simp add: split_beta)
 apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)