Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/AList.thy
changeset 46507 1b24c24017dd
parent 46238 9ace9e5b79be
child 47397 d654c73e4b12 
--- a/src/HOL/Library/AList.thy	Thu Feb 16 22:18:28 2012 +0100
+++ b/src/HOL/Library/AList.thy	Thu Feb 16 22:53:24 2012 +0100
@@ -135,7 +135,7 @@
 lemma updates_twist [simp]:
  "k \<notin> set ks \<Longrightarrow> 
   map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
-  by (simp add: updates_conv' update_conv' map_upds_twist)
+  by (simp add: updates_conv' update_conv')
 
 lemma updates_apply_notin[simp]:
  "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
isabelle