src/HOL/Data_Structures/Tree_Map.thy
changeset 68020 6aade817bee5
parent 67965 aaa31cd0caef
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  "delete x (Node l (a,b) r) = (case cmp x a of
     1.5    LT \<Rightarrow> Node (delete x l) (a,b) r |
     1.6    GT \<Rightarrow> Node l (a,b) (delete x r) |
     1.7 -  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
     1.8 +  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = split_min r in Node l ab' r')"
     1.9  
    1.10  
    1.11  subsection "Functional Correctness Proofs"
    1.12 @@ -40,7 +40,7 @@
    1.13  
    1.14  lemma inorder_delete:
    1.15    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.16 -by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
    1.17 +by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
    1.18  
    1.19  interpretation Map_by_Ordered
    1.20  where empty = Leaf and lookup = lookup and update = update and delete = delete