Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Data_Structures/RBT_Set.thy
changeset 68998 818898556504
parent 68440 6826718f732d
child 70571 e72daea2aab6 
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -299,7 +299,7 @@
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
   hence "height t / 2 \<le> log 2 (size1 t)"
-    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
+    by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed
isabelle