src/HOL/Library/Tree_Multiset.thy

--- a/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 18:13:44 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 20:21:40 2015 +0200
@@ -23,6 +23,9 @@
 lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
 by (induction t) auto
 
+lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
+by(induction t arbitrary: x) auto
+
 lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
 by (induction t) (auto simp: ac_simps)