src/HOL/Data_Structures/RBT.thy
 changeset 68413 b56ed5010e69 parent 67910 b42473502373
```     1.1 --- a/src/HOL/Data_Structures/RBT.thy	Mon Jun 11 08:15:43 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/RBT.thy	Mon Jun 11 16:29:27 2018 +0200
1.3 @@ -10,8 +10,8 @@
1.4
1.5  type_synonym 'a rbt = "('a,color)tree"
1.6
1.7 -abbreviation R where "R l a r \<equiv> Node Red l a r"
1.8 -abbreviation B where "B l a r \<equiv> Node Black l a r"
1.9 +abbreviation R where "R l a r \<equiv> Node l a Red r"
1.10 +abbreviation B where "B l a r \<equiv> Node l a Black r"
1.11
1.12  fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.13  "baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
1.14 @@ -25,7 +25,7 @@
1.15
1.16  fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.17  "paint c Leaf = Leaf" |
1.18 -"paint c (Node _ l a r) = Node c l a r"
1.19 +"paint c (Node l a _ r) = Node l a c r"
1.20
1.21  fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.22  "baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
```