# HG changeset patch
# User nipkow
# Date 1504110923 -7200
# Node ID 2d24e2c021302421476332e42e44c3e0f4a6fdee
# Parent  b8a6f933722988c43514ef396211c2ee5b90e507
added lemma

diff -r b8a6f9337229 -r 2d24e2c02130 src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Tue Aug 29 17:01:11 2017 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Aug 30 18:35:23 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