# HG changeset patch
# User nipkow
# Date 1577440455 -3600
# Node ID 7a0a6c56015e0a77ed037661f07491d80791eb58
# Parent  a956b769903e770655024cd9e94d178312e1f640
tuned

diff -r a956b769903e -r 7a0a6c56015e src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Dec 24 21:50:02 2019 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Dec 27 10:54:15 2019 +0100
@@ -291,7 +291,7 @@
 by (cases c) auto
 
 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
-  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
+  height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
 by(induction t) (auto split: if_split_asm)
 
 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "