discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;

tuned headers;

updated to polyml-5.3.0, which is presently known as the most robust version;

explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;

always test/clear Multithreading.interrupted, indepently of thread attributes; tuned;

added Multithreading.interrupted (cf. java.lang.Thread.interrupted);

more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);

more tracing information via Par_List.map_name;

clarified bootstrapping of structure TimeLimit;

more scalable collections of tasks, notably for totality of known group members; tuned;

tuned signature; tuned;

merged

prefer p2e before e2p; use measure_unique_Int_stable_vimage;

add auto support for AE_mp

add borel_fubini_integrable; remove unused bijectivity rules for measureable functions

parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;

Task_Queue.update_timing: more precise treatment of interruptibility; Task_Queue.waiting: potentially expensive wait dependencies are subject to trace flag;

Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;

thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;

tuned comments;

clarified Proofterm.proofs_enabled;

explicit is better than implicit;

tuned odd conditional expression;

eliminated slightly odd abstract type Task_Queue.deps; tuned signature; tuned;

merged

Introduction of metis calls and other cosmetic modifications.

merged

avoid ML structure aliases (especially single-letter abbreviations)

making the bash script swipl_version closer to Isabelle's conventional bash scripts

the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.