# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1483547638 0
# Node ID 8cac34b3dcd007ed485fb5885a223ae5101477cb
# Parent  223b2ebdda791cbd506d31ec12bc644962e07426# Parent  346d5158fc2f94cff5d71a585f38372d33faf23f
Merge

diff -r 223b2ebdda79 -r 8cac34b3dcd0 src/HOL/Library/Tree.thy
--- 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>