# HG changeset patch
# User nipkow
# Date 1504119045 -7200
# Node ID b17d41779768c997db17336667000a68513cc23e
# Parent  39257f39c7daf4aa124796d34a51dd931131d7c8# Parent  2d24e2c021302421476332e42e44c3e0f4a6fdee
merged

diff -r 39257f39c7da -r b17d41779768 src/HOL/Library/Tree_Multiset.thy
--- 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