more compact name
authornipkow
Wed Jun 17 18:13:44 2015 +0200 (2015-06-17)
changeset 60498c8141ac6f03f
parent 60497 010c26e24c72
child 60503 47df24e05b1c
child 60505 9e6584184315
more compact name
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Jun 17 17:33:22 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 18:13:44 2015 +0200
     1.3 @@ -884,7 +884,7 @@
     1.4    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
     1.5    by simp
     1.6  
     1.7 -lemma set_mset_image_mset [simp]:
     1.8 +lemma set_image_mset [simp]:
     1.9    "set_mset (image_mset f M) = image f (set_mset M)"
    1.10    by (induct M) simp_all
    1.11  
    1.12 @@ -928,7 +928,7 @@
    1.13  *}
    1.14  
    1.15  lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
    1.16 -  by (metis mem_set_mset_iff set_mset_image_mset)
    1.17 +by (metis mem_set_mset_iff set_image_mset)
    1.18  
    1.19  functor image_mset: image_mset
    1.20  proof -