option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;

prefer outdegree in comparison again (cf. 88c96e836ed6) -- NB: big jobs might hide behind small ones in this naive queuing scheme;

more tight representation of command timing; tuned signatures; tuned;

prefer comparison of session timing, if this is known already; some odd workarounds to prevent crashes due to TreeSet.- sometimes not deleting the element;

proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);

support nested Thy_Syntax.element; more explicit Keyword.is_proof_body; tuned;

back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;

help JVM to cope with large symbolic structures;

improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);

read logs from failed sessions as well; proper output base directory (which is two steps upwards);

recover timing information from old log files; use session timing for queue ordering; pass command timings to ML process (still unused);

suppress timing message in full PIDE protocol -- this is for batch build;

support for build passing timings from Scala to ML;

support for prescient timing information within command transactions;

emit command_timing properties into build log; tuned;

generate Isar proof if Metis appears to be too slow

swap slices so that the last slice is more complete (for minimization)

tuning

ensure all conjecture clauses are in the graph -- to prevent exceptions later

generalize syntax of SPASS proofs

tweaked hack some more

more simplifying constructors

remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)

more precise error

improved hack

upgraded to Alt-Ergo 0.95

don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary

trust preplayed proof in Mirabelle

added case taken out by mistake

tuning (removed redundant datatype)