# HG changeset patch
# User nipkow
# Date 1484769819 -3600
# Node ID 1cbfe46ad6b111befe861092777ecfc19a3da0c6
# Parent  31044168af84dc23f4c0a8c28a5f97f2f65c3608
tuned

diff -r 31044168af84 -r 1cbfe46ad6b1 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Jan 18 17:56:52 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Wed Jan 18 21:03:39 2017 +0100
@@ -357,7 +357,7 @@
 text \<open>The internal path length of a tree:\<close>
 
 lemma ipl_if_complete: "complete t
-  \<Longrightarrow> ipl t = (let n = height t in 2 + n*2^n - 2^(n+1))"
+  \<Longrightarrow> ipl t = (let h = height t in 2 + h*2^h - 2^(h+1))"
 proof(induction t)
   case (Node l x r)
   have *: "2^(n+1) \<le> 2 + n*2^n" for n :: nat