# HG changeset patch
# User nipkow
# Date 1483536379 -3600
# Node ID 346d5158fc2f94cff5d71a585f38372d33faf23f
# Parent  1ddc262514b8d5d6ccc8438fba175c340feec6bc# Parent  23c56f483775fdcfbb9fe7bf730d1cc137892279
merged

diff -r 1ddc262514b8 -r 346d5158fc2f src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Wed Jan 04 14:26:19 2017 +0100
@@ -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>