--- a/src/HOL/Data_Structures/RBT.thy Fri Dec 27 16:02:23 2019 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Sat Dec 28 00:15:43 2019 +0100
@@ -48,7 +48,7 @@
t23 \<Rightarrow> R t1 a (R t23 c t4))" |
"combine (B t1 a t2) (B t3 c t4) =
(case combine t2 t3 of
- R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
+ R u2 b u3 \<Rightarrow> R (B t1 a u2) b (B u3 c t4) |
t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)"
--- a/src/HOL/Data_Structures/RBT_Set.thy Fri Dec 27 16:02:23 2019 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sat Dec 28 00:15:43 2019 +0100
@@ -195,7 +195,7 @@
lemma invh_baldL_invc:
"\<lbrakk> invh l; invh r; bheight l + 1 = bheight r; invc r \<rbrakk>
- \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
+ \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
by (induct l a r rule: baldL.induct)
(auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)