changeset 57530 | 439f881c8744 |
parent 57450 | 2baecef3207f |
child 57569 | e20a999f7161 |
--- a/src/HOL/Library/Tree.thy Mon Jul 07 16:06:46 2014 +0200 +++ b/src/HOL/Library/Tree.thy Mon Jul 07 17:01:11 2014 +0200 @@ -14,6 +14,9 @@ lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)" by (cases t) auto +lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)" +by auto + fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where "subtrees Leaf = {Leaf}" | "subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)"