Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Mon, 23 Sep 2019 08:43:52 +0200
changeset 70745 be8e617b6eb3
parent 70744 b605c9cf82a2
child 70746 cf7b5020c207
child 70747 548420d389ea
tuned
src/HOL/Data_Structures/Tree2.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle