Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified proof
authornipkow
Sun, 10 Oct 2010 16:34:20 +0200
changeset 39976 2474347538b8
parent 39975 7c50d5ca5c04
child 39977 c9cbc16e93ce
simplified proof
src/HOL/MicroJava/Comp/AuxLemmas.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle