src/HOL/Data_Structures/RBT_Set.thy
changeset 67118 ccab07d1196c
parent 66088 c9c9438cfc0f
child 67963 9541f2c5ce8d
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
     1.3 @@ -303,7 +303,7 @@
     1.4      by (simp add: powr_realpow bheight_size_bound rbt_def)
     1.5    finally have "2 powr (height t / 2) \<le> size1 t" .
     1.6    hence "height t / 2 \<le> log 2 (size1 t)"
     1.7 -    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
     1.8 +    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
     1.9    thus ?thesis by simp
    1.10  qed
    1.11