--- a/src/HOL/Library/Tree_Multiset.thy Wed Aug 30 15:53:35 2017 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy Wed Aug 30 20:50:45 2017 +0200
@@ -19,6 +19,9 @@
"subtrees_mset (Node l x r) = add_mset (Node l x r) (subtrees_mset l + subtrees_mset r)"
+lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
by(induction t) auto
@@ -40,7 +43,6 @@
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
by (induction t) (simp_all add: ac_simps)
-
lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
by(induction t) auto