# HG changeset patch
# User wenzelm
# Date 1683323431 -7200
# Node ID 93999ffdb9dd7f81ebc06101bed38ad9b6f40ee7
# Parent  ab6e4085a19da9ead588442d7d5cf3f3e855c407
more operations;

diff -r ab6e4085a19d -r 93999ffdb9dd src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Fri May 05 23:48:14 2023 +0200
+++ b/src/Pure/General/change_table.ML	Fri May 05 23:50:31 2023 +0200
@@ -30,6 +30,9 @@
   val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
   val delete_safe: key -> 'a T -> 'a T
+  val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
+  val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list T -> 'a list T
+  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
 end;
 
 functor Change_Table(Key: KEY): CHANGE_TABLE =
@@ -153,7 +156,10 @@
 fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
 fun delete_safe key        = change_table key (Table.delete_safe key);
 
+fun insert_list eq (key, x) = change_table key (Table.insert_list eq (key, x));
+fun remove_list eq (key, x) = change_table key (Table.remove_list eq (key, x));
+fun update_list eq (key, x) = change_table key (Table.update_list eq (key, x));
+
 end;
 
 structure Change_Table = Change_Table(type key = string val ord = fast_string_ord);
-