| changeset 70744 | b605c9cf82a2 |
| parent 70742 | e21c6b677c79 |
| child 70745 | be8e617b6eb3 |
| 70743:342b0a1fc86d | 70744:b605c9cf82a2 |
|---|---|
37 by (simp add: size1_size) |
37 by (simp add: size1_size) |
38 |
38 |
39 lemma finite_set_tree[simp]: "finite(set_tree t)" |
39 lemma finite_set_tree[simp]: "finite(set_tree t)" |
40 by(induction t) auto |
40 by(induction t) auto |
41 |
41 |
42 lemma set_tree_empty: "set_tree t = {} \<longleftrightarrow> t = Leaf" |
|
43 by (cases t) auto |
|
44 |
|
42 end |
45 end |