tuned
authornipkow
Mon Sep 23 08:43:52 2019 +0200 (4 weeks ago ago)
changeset 70935be8e617b6eb3
parent 70934 b605c9cf82a2
child 70936 548420d389ea
child 70937 cf7b5020c207
tuned
src/HOL/Data_Structures/Tree2.thy
     1.1 --- a/src/HOL/Data_Structures/Tree2.thy	Mon Sep 23 07:57:58 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Mon Sep 23 08:43:52 2019 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  lemma finite_set_tree[simp]: "finite(set_tree t)"
     1.5  by(induction t) auto
     1.6  
     1.7 -lemma set_tree_empty: "set_tree t = {} \<longleftrightarrow> t = Leaf"
     1.8 +lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
     1.9  by (cases t) auto
    1.10  
    1.11  end