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.
Merge
authorpaulson <lp15@cam.ac.uk>
Wed, 04 Jan 2017 16:33:58 +0000
changeset 64774 8cac34b3dcd0
parent 64773 223b2ebdda79 (current diff)
parent 64772 346d5158fc2f (diff)
child 64781 31b5a28cadbc
Merge
--- a/src/HOL/Library/Tree.thy	Wed Jan 04 16:18:50 2017 +0000
+++ b/src/HOL/Library/Tree.thy	Wed Jan 04 16:33:58 2017 +0000
@@ -356,8 +356,6 @@
 lemma wbalanced_subtrees: "\<lbrakk> wbalanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> wbalanced s"
 using [[simp_depth_limit=1]] by(induction t arbitrary: s) auto
 
-(* show wbalanced \<Longrightarrow> balanced and use that in Balanced.thy *)
-
 
 subsection \<open>@{const path_len}\<close>
isabelle