# 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 "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith
     also have "\<dots> \<le> 2 ^ height r + 2 ^ height r" using True by simp
-    also have "\<dots> \<le> 2 ^ height (Node l a r)"
+    also have "\<dots> = 2 ^ height (Node l a r)"
       using True by (auto simp: max_def mult_2)
     finally show ?thesis .
   next