| changeset 39976 | 2474347538b8 |
| parent 39917 | b85bfa89a387 |
| child 44890 | 22f665a2e91c |
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Sun Oct 10 18:42:13 2010 +0700 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Sun Oct 10 16:34:20 2010 +0200 @@ -86,7 +86,7 @@ lemma map_upds_distinct [simp]: "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs" -apply (induct ys arbitrary: f vs rule: distinct.induct) +apply (induct ys arbitrary: f vs) apply simp apply (case_tac vs) apply simp_all