# HG changeset patch
# User haftmann
# Date 1291412060 -3600
# Node ID a370b0fb6f099a6fe89faa03df33525f835229a9
# Parent  1d46d893d682ed499a7bbbcd21f63540f0dad76c
lemma multiset_of_rev

diff -r 1d46d893d682 -r a370b0fb6f09 src/HOL/Library/Multiset.thy
--- 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)