src/HOL/Library/AList_Mapping.thy
changeset 51161 6ed12ae3b3e1
parent 49929 70300f1b6835
child 57850 34382a1f37d6
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  proof -
     1.5    have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
     1.6      by (auto simp add: image_def intro!: bexI)
     1.7 -  show ?thesis apply transfer 
     1.8 +  show ?thesis apply transfer
     1.9    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
    1.10  qed
    1.11