# HG changeset patch
# User nipkow
# Date 1521723195 -3600
# Node ID b42473502373ba74198f48fa8705c965bf3f7041
# Parent  f55b07f4d1eea66607c2641b5a78c07580e88b2a
make baliL and baliR symmetric

diff -r f55b07f4d1ee -r b42473502373 src/HOL/Data_Structures/RBT.thy
--- 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