| changeset 70745 | be8e617b6eb3 |
| parent 70744 | b605c9cf82a2 |
| child 70755 | 3fb16bed5d6c |
--- a/src/HOL/Data_Structures/Tree2.thy Mon Sep 23 07:57:58 2019 +0200 +++ b/src/HOL/Data_Structures/Tree2.thy Mon Sep 23 08:43:52 2019 +0200 @@ -39,7 +39,7 @@ lemma finite_set_tree[simp]: "finite(set_tree t)" by(induction t) auto -lemma set_tree_empty: "set_tree t = {} \<longleftrightarrow> t = Leaf" +lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf" by (cases t) auto end