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.

merged

scala serializer adds parentheses around function literals

made SML/NJ happy

term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)

refined Task_Queue.dequeue_deps (more incremental);

maintain Task_Queue.group within Task_Queue.task; Task_Queue.dummy_task: id = 0 in accordance to Document.no_id etc.; tuned signature;

tuned comment;

Future.join_results: discontinued post-hoc recording of dynamic dependencies; abstract Task_Queue.deps; tuned signature; tuned;

more informative task timing: some dependency tracking;

refined task timing: joining vs. waiting; tuned;

simplified trace;

more specific Goal.fork_name;

name "passive" tasks (practically lazy values);

tuned trivial cases;

tuned signature; tuned vacous forks;

support named tasks, for improved tracing;