added lemma

--- 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)"