changeset 68411 | d8363de26567 |
parent 67967 | 5a4280946a25 |
child 68413 | b56ed5010e69 |
68410:4e27f5c361d2 | 68411:d8363de26567 |
---|---|
31 by (simp_all add: size1_def) |
31 by (simp_all add: size1_def) |
32 |
32 |
33 lemma size1_ge0[simp]: "0 < size1 t" |
33 lemma size1_ge0[simp]: "0 < size1 t" |
34 by (simp add: size1_def) |
34 by (simp add: size1_def) |
35 |
35 |
36 lemma finite_set_tree[simp]: "finite(set_tree t)" |
|
37 by(induction t) auto |
|
38 |
|
36 end |
39 end |