# HG changeset patch
# User nipkow
# Date 1434557624 -7200
# Node ID c8141ac6f03f09ab80551034cf52fd26c758d387
# Parent  010c26e24c7261a978869e645cffcfe9b2bbbdec
more compact name

diff -r 010c26e24c72 -r c8141ac6f03f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jun 17 17:33:22 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 18:13:44 2015 +0200
@@ -884,7 +884,7 @@
   "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   by simp
 
-lemma set_mset_image_mset [simp]:
+lemma set_image_mset [simp]:
   "set_mset (image_mset f M) = image f (set_mset M)"
   by (induct M) simp_all
 
@@ -928,7 +928,7 @@
 *}
 
 lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
-  by (metis mem_set_mset_iff set_mset_image_mset)
+by (metis mem_set_mset_iff set_image_mset)
 
 functor image_mset: image_mset
 proof -