UNIV_code now named UNIV_apply

attempt for more concise setup of non-etacontracting binders

moved abstract algebra section to the end

merged

Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy

merged

swapped bootstrap order of UNION/Union and INTER/Inter in theory Set

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.;

moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;

moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;

removed obsolete CVS Ids;

merged

merged

deftab: only process theorems on demand

no SAME exceptions in uncritical code

merged

less digestible

refined outline structure

replaced usedir option -Q by more fine-grained -q;

merged

merged

closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text

merged

merged

simplification of locale interfaces

additional preprocessor rule

added code_unfold_post attribute

more accessors to unfold simpset

clarified code

prefer code_inline over code_unfold; use code_unfold_post where appropriate

tuned code annotations

more canonical import

merged

merged

refinement of lattice classes

removed outdated comment

Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);