added lemma
authornipkow
Mon Jun 11 08:15:43 2018 +0200 (11 months ago)
changeset 68411d8363de26567
parent 68410 4e27f5c361d2
child 68412 07f8c09e3f79
child 68413 b56ed5010e69
child 68416 33114721ac9a
child 68424 02e5a44ffe7d
added lemma
src/HOL/Data_Structures/Tree2.thy
     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