--- a/src/HOL/Library/Multiset.thy Fri Dec 03 22:34:20 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 03 22:34:20 2010 +0100
@@ -725,7 +725,7 @@
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
by (induct x) auto
-lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
+lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
by (induct x) auto
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
@@ -739,6 +739,10 @@
"multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
by (induct xs) simp_all
+lemma multiset_of_rev [simp]:
+ "multiset_of (rev xs) = multiset_of xs"
+ by (induct xs) simp_all
+
lemma surj_multiset_of: "surj multiset_of"
apply (unfold surj_def)
apply (rule allI)