src/HOL/Data_Structures/AList_Upd_Del.thy

--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Sep 21 23:22:11 2015 +0200
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Sep 22 08:38:25 2015 +0200
@@ -77,7 +77,7 @@
   upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
 by(induction ps) (auto simp: sorted_lems)
 
-lemmas upd_list_sorteds = upd_list_sorted1 upd_list_sorted2
+lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
 
 (*
 lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"