src/HOL/Data_Structures/AVL_Set.thy
changeset 70350 571ae57313a4
parent 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -545,7 +545,8 @@
     1.4    have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
     1.5    hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
     1.6    also have "\<dots> \<le> log \<phi> (size1 t)"
     1.7 -    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>  by simp
     1.8 +    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>
     1.9 +    by (simp add: le_log_of_power) 
    1.10    also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
    1.11      by(simp add: log_base_change[of 2 \<phi>])
    1.12    finally show ?thesis .