# HG changeset patch # User nipkow # Date 1484825986 -3600 # Node ID 3fb4d7d002305f0b2f3503c91a2e067e10f7325f # Parent 1cbfe46ad6b111befe861092777ecfc19a3da0c6 tuned diff -r 1cbfe46ad6b1 -r 3fb4d7d00230 src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Wed Jan 18 21:03:39 2017 +0100 +++ b/src/HOL/Library/Tree.thy Thu Jan 19 12:39:46 2017 +0100 @@ -147,7 +147,7 @@ have "size1(Node l a r) = size1 l + size1 r" by simp also have "\ \ 2 ^ height l + 2 ^ height r" using Node.IH by arith also have "\ \ 2 ^ height r + 2 ^ height r" using True by simp - also have "\ \ 2 ^ height (Node l a r)" + also have "\ = 2 ^ height (Node l a r)" using True by (auto simp: max_def mult_2) finally show ?thesis . next