src/HOL/Data_Structures/Tree_Map.thy
changeset 61224 759b5299a9f2
parent 61203 a8a8eca85801
child 61231 cc6969542f8d
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Sep 21 23:22:11 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Tue Sep 22 08:38:25 2015 +0200
     1.3 @@ -33,7 +33,8 @@
     1.4  
     1.5  subsection "Functional Correctness Proofs"
     1.6  
     1.7 -lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
     1.8 +lemma lookup_eq:
     1.9 +  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    1.10  apply (induction t)
    1.11  apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    1.12  done
    1.13 @@ -41,7 +42,7 @@
    1.14  
    1.15  lemma inorder_update:
    1.16    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    1.17 -by(induction t) (auto simp: upd_list_sorteds sorted_lems)
    1.18 +by(induction t) (auto simp: upd_list_simps)
    1.19  
    1.20  
    1.21  lemma del_minD: