src/HOL/Library/Multiset.thy
changeset 40950 a370b0fb6f09
parent 40606 af1a0b0c6202
child 40968 a6fcd305f7dc
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Dec 03 22:34:20 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Dec 03 22:34:20 2010 +0100
     1.3 @@ -725,7 +725,7 @@
     1.4  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
     1.5  by (induct x) auto
     1.6  
     1.7 -lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
     1.8 +lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
     1.9  by (induct x) auto
    1.10  
    1.11  lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
    1.12 @@ -739,6 +739,10 @@
    1.13    "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
    1.14    by (induct xs) simp_all
    1.15  
    1.16 +lemma multiset_of_rev [simp]:
    1.17 +  "multiset_of (rev xs) = multiset_of xs"
    1.18 +  by (induct xs) simp_all
    1.19 +
    1.20  lemma surj_multiset_of: "surj multiset_of"
    1.21  apply (unfold surj_def)
    1.22  apply (rule allI)