tuned whitespace;
authorwenzelm
Sun, 03 Aug 2014 17:38:59 +0200
changeset 57850 34382a1f37d6
parent 57849 6d8f97d555d8
child 57851 33b7372e87ad
tuned whitespace;
src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:33:38 2014 +0200
+++ b/src/HOL/Library/AList_Mapping.thy	Sun Aug 03 17:38:59 2014 +0200
@@ -60,7 +60,7 @@
   have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
     by (auto simp add: image_def intro!: bexI)
   show ?thesis apply transfer
-  by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
+    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
 qed
 
 lemma [code nbe]: