# HG changeset patch
# User wenzelm
# Date 1681161707 -7200
# Node ID 1a9decb8bfbcf4151e86a53c96a2f97827d642a4
# Parent  8ee97b3841cc4ba7938c9fb1ccf29148dec1b191
more NEWS;

diff -r 8ee97b3841cc -r 1a9decb8bfbc NEWS
--- a/NEWS	Mon Apr 10 23:11:04 2023 +0200
+++ b/NEWS	Mon Apr 10 23:21:47 2023 +0200
@@ -292,6 +292,12 @@
   - The new "size" operation works with constant time complexity and
     minimal space overhead: small structures have no size descriptor.
 
+  - Various internal interfaces now use scalable Set() instances instead
+    of plain list, notably Thm.hyps_of and Thm.shyps_of. Minor
+    INCOMPATIBILITY: use e.g. Termset.dest to adapt the result, better
+    use proper Termset operations such as Termset.exists or Termset.fold
+    without the overhead of destruction.
+
 * Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object
 size on the heap in bytes. The latter works simultaneously on multiple
 objects, taking implicit sharing of values into account. Examples for