author | nipkow |
Thu, 26 Sep 2019 21:22:58 +0200 | |
changeset 70762 | d4a23cc9aabc |
parent 70761 | a9312914081f |
child 70763 | 5fae55752c70 |
--- 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