changeset 57850 | 34382a1f37d6 |
parent 51161 | 6ed12ae3b3e1 |
child 58881 | b9556a055632 |
--- 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]: