src/HOL/Library/Tree_Real.thy
changeset 70350 571ae57313a4
parent 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -19,7 +19,7 @@
     1.4  by (simp add: le_log2_of_power min_height_size1)
     1.5  
     1.6  lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
     1.7 -by (simp add: log2_of_power_eq size1_if_complete)
     1.8 +by (simp add: size1_if_complete)
     1.9  
    1.10  lemma min_height_size1_log_if_incomplete:
    1.11    "\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"