# HG changeset patch
# User nipkow
# Date 1404745271 -7200
# Node ID 439f881c8744388b94d73d7556107c5d514ca8d5
# Parent  5e83df79eaa0d4bd3f723f496c2ce4af42a32e1b
added lemma

diff -r 5e83df79eaa0 -r 439f881c8744 src/HOL/Library/Tree.thy
--- 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)"