future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;

added cancel_proofs, based on task groups of "entered" proofs;

added pending_groups -- accumulates task groups of local derivations only;

added cancel_group;

merged

schedule_futures: tuned final consolidation, explicit after_load phase;

load_thy: explicit after_load phase for presentation;

excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;

slightly more robust matching of session name;

merged

fixed proof involving dvd;

tuned;

added force_result;

use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;

simplified join_proofs;

merged

added split_thy_path;

added running task markup;

tuned;

merged

merged

merged.

fix proof broken by changes in dvd theory

merged.

remove type-specific proofs

add lemma dvd_diff to class comm_ring_1

add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1

move lemmas mult_minus{left,right} inside class ring