--- a/src/HOL/Data_Structures/RBT.thy Wed Mar 21 20:17:25 2018 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Thu Mar 22 13:53:15 2018 +0100
@@ -19,8 +19,8 @@
"baliL t1 a t2 = B t1 a t2"
fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"baliR t1 a t2 = B t1 a t2"
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where