changeset 44890 | 22f665a2e91c |
parent 39976 | 2474347538b8 |
child 52866 | 438f578ef1d9 |
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Sep 12 07:55:43 2011 +0200 @@ -81,7 +81,7 @@ "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs" apply (induct xs arbitrary: f vs) apply simp -apply fastsimp +apply fastforce done lemma map_upds_distinct [simp]: