# HG changeset patch # User nipkow # Date 1538592959 -7200 # Node ID 919a1b23c192300c09da05ee625768fe5b713dcc # Parent 163626ddaa1968642a1622301989741b3943763e tuned diff -r 163626ddaa19 -r 919a1b23c192 src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Wed Oct 03 13:20:05 2018 +0200 +++ b/src/HOL/Library/Tree.thy Wed Oct 03 20:55:59 2018 +0200 @@ -351,7 +351,7 @@ have "(2::nat) ^ height t \ 2 ^ height t'" proof - have "2 ^ height t = size1 t" - using True by (simp add: complete_iff_height size1_if_complete) + using True by (simp add: size1_if_complete) also have "\ \ size1 t'" using assms(2) by(simp add: size1_size) also have "\ \ 2 ^ height t'" by (rule size1_height) finally show ?thesis .