# HG changeset patch
# User nipkow
# Date 1569221032 -7200
# Node ID be8e617b6eb34498cf6cc9bed317fdd7c766c80f
# Parent  b605c9cf82a2c0215f1640a5520a3756e3779be2
tuned

diff -r b605c9cf82a2 -r be8e617b6eb3 src/HOL/Data_Structures/Tree2.thy
--- 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