src/HOL/Data_Structures/AVL_Map.thy
changeset 68413 b56ed5010e69
parent 68023 75130777ece4
child 68422 0a3a36fa1d63
     1.1 --- a/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -9,16 +9,16 @@
     1.4  begin
     1.5  
     1.6  fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
     1.7 -"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
     1.8 -"update x y (Node h l (a,b) r) = (case cmp x a of
     1.9 -   EQ \<Rightarrow> Node h l (x,y) r |
    1.10 +"update x y Leaf = Node Leaf (x,y) 1 Leaf" |
    1.11 +"update x y (Node l (a,b) h r) = (case cmp x a of
    1.12 +   EQ \<Rightarrow> Node l (x,y) h r |
    1.13     LT \<Rightarrow> balL (update x y l) (a,b) r |
    1.14     GT \<Rightarrow> balR l (a,b) (update x y r))"
    1.15  
    1.16  fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
    1.17  "delete _ Leaf = Leaf" |
    1.18 -"delete x (Node h l (a,b) r) = (case cmp x a of
    1.19 -   EQ \<Rightarrow> del_root (Node h l (a,b) r) |
    1.20 +"delete x (Node l (a,b) h r) = (case cmp x a of
    1.21 +   EQ \<Rightarrow> del_root (Node l (a,b) h r) |
    1.22     LT \<Rightarrow> balR (delete x l) (a,b) r |
    1.23     GT \<Rightarrow> balL l (a,b) (delete x r))"
    1.24