equal
deleted
inserted
replaced
292 - Data representation is more compact than before, approx. 85% .. 110% |
292 - Data representation is more compact than before, approx. 85% .. 110% |
293 of a plain list (e.g. see structure AList or Ord_List, respectively). |
293 of a plain list (e.g. see structure AList or Ord_List, respectively). |
294 |
294 |
295 - The new "size" operation works with constant time complexity and |
295 - The new "size" operation works with constant time complexity and |
296 minimal space overhead: small structures have no size descriptor. |
296 minimal space overhead: small structures have no size descriptor. |
297 |
|
298 - Various internal interfaces now use scalable Set() instances instead |
|
299 of plain list, notably Thm.hyps_of and Thm.shyps_of. Minor |
|
300 INCOMPATIBILITY: use e.g. Termset.dest to adapt the result, better |
|
301 use proper Termset operations such as Termset.exists or Termset.fold |
|
302 without the overhead of destruction. |
|
303 |
297 |
304 * Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object |
298 * Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object |
305 size on the heap in bytes. The latter works simultaneously on multiple |
299 size on the heap in bytes. The latter works simultaneously on multiple |
306 objects, taking implicit sharing of values into account. Examples for |
300 objects, taking implicit sharing of values into account. Examples for |
307 the default 64_32 platform (4 bytes per machine word): |
301 the default 64_32 platform (4 bytes per machine word): |