src/HOL/Data_Structures/RBT_Map.thy
changeset 68413 b56ed5010e69
parent 64960 8be78855ee7a
child 68415 d74ba11680d4
     1.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
     1.5  where
     1.6  "del x Leaf = Leaf" |
     1.7 -"del x (Node c t1 (a,b) t2) = (case cmp x a of
     1.8 +"del x (Node t1 (a,b) c t2) = (case cmp x a of
     1.9    LT \<Rightarrow> delL x t1 (a,b) t2 |
    1.10    GT \<Rightarrow> delR x t1 (a,b) t2 |
    1.11    EQ \<Rightarrow> combine t1 t2)" |