author | nipkow |
Wed, 04 Jan 2017 14:26:19 +0100 | |
changeset 64772 | 346d5158fc2f |
parent 64770 | 1ddc262514b8 (current diff) |
parent 64771 | 23c56f483775 (diff) |
child 64774 | 8cac34b3dcd0 |
--- 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>