merged

dropped add_registration interface in locale

Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM

Tests for executability of "prime"

less ambitious settings;

future_job: more robust Exn.capture outside thread attribute change;

shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;

future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group; control combinators: paranoia eta-expansion to ensure proper operational semantics;

maintain Future.worker_group as management data; cancel_thy: refer to proper task group; tuned;

join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;

simultaneous join_proofs; removed obsolete promises_of;

map: subgroup of worker_group;

added worker_group; fork: default to subgroup of worker_group; removed obsolete fork_local; join/get_result: cumulative flattened exceptions; map: subgroup of worker_group;

support for nested groups -- cancellation is propagated to peers and subgroups; added is_canceled; tuned;

added flatten/flatten_list -- supercedes internal plain_exns; represent empty failure as EXCEPTIONS [] instead of Interrupt;

propagate exceptions within future groups; Future.map: inherit group;

less ambitious ML_OPTIONS;

disabled macbroy6 -- hardware repair;

tuned;

tuned tracing; provide spare worker threads to saturate hardware while other workers wait during join;

prefer simultaneous join -- for improved scheduling;

tuned dequeu_towards: try immediate tasks before expensive all_preds;

Display.pretty_thm now requires a proper context;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;