diff -r 342b0a1fc86d -r b605c9cf82a2 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Sun Sep 22 19:04:11 2019 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Mon Sep 23 07:57:58 2019 +0200
@@ -39,4 +39,7 @@
 lemma finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto
 
+lemma set_tree_empty: "set_tree t = {} \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
 end