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" |