src/HOL/Library/Tree_Real.thy

--- a/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
@@ -19,7 +19,7 @@
 by (simp add: le_log2_of_power min_height_size1)
 
 lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
-by (simp add: log2_of_power_eq size1_if_complete)
+by (simp add: size1_if_complete)
 
 lemma min_height_size1_log_if_incomplete:
   "\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"