simplified proof
authornipkow
Sun Oct 10 16:34:20 2010 +0200 (2010-10-10)
changeset 399762474347538b8
parent 39975 7c50d5ca5c04
child 39977 c9cbc16e93ce
simplified proof
src/HOL/MicroJava/Comp/AuxLemmas.thy
     1.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Sun Oct 10 18:42:13 2010 +0700
     1.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Sun Oct 10 16:34:20 2010 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  lemma map_upds_distinct [simp]: 
     1.6    "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
     1.7 -apply (induct ys arbitrary: f vs rule: distinct.induct)
     1.8 +apply (induct ys arbitrary: f vs)
     1.9  apply simp
    1.10  apply (case_tac vs)
    1.11  apply simp_all