diff -r 4e27f5c361d2 -r d8363de26567 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Sat Jun 09 21:52:16 2018 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Mon Jun 11 08:15:43 2018 +0200
@@ -33,4 +33,7 @@
 lemma size1_ge0[simp]: "0 < size1 t"
 by (simp add: size1_def)
 
+lemma finite_set_tree[simp]: "finite(set_tree t)"
+by(induction t) auto
+
 end