# HG changeset patch
# User nipkow
# Date 1569525778 -7200
# Node ID d4a23cc9aabc29c65579276b6a07c45ed8d07e9d
# Parent  a9312914081fd16a2ccd3f42832444cd98e89f1a
added lemma

diff -r a9312914081f -r d4a23cc9aabc src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Thu Sep 26 15:25:51 2019 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Thu Sep 26 21:22:58 2019 +0200
@@ -31,4 +31,7 @@
 lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
+lemma set_inorder[simp]: "set (inorder t) = set_tree t"
+by (induction t) auto
+
 end