src/HOL/Data_Structures/Tree2.thy
changeset 68411 d8363de26567
parent 67967 5a4280946a25
child 68413 b56ed5010e69
     1.1 --- a/src/HOL/Data_Structures/Tree2.thy	Sat Jun 09 21:52:16 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Mon Jun 11 08:15:43 2018 +0200
     1.3 @@ -33,4 +33,7 @@
     1.4  lemma size1_ge0[simp]: "0 < size1 t"
     1.5  by (simp add: size1_def)
     1.6  
     1.7 +lemma finite_set_tree[simp]: "finite(set_tree t)"
     1.8 +by(induction t) auto
     1.9 +
    1.10  end