--- a/src/HOL/Data_Structures/RBT.thy Sun Nov 15 11:27:55 2015 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Sun Nov 15 12:45:28 2015 +0100
@@ -41,12 +41,14 @@
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"combine Leaf t = t" |
"combine t Leaf = t" |
-"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
- R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
- 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) |
- t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
+"combine (R t1 a t2) (R t3 c t4) =
+ (case combine t2 t3 of
+ R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
+ 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) |
+ t23 \<Rightarrow> balL 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)"