setmp_noncritical;

dequeue_towards: return bound for unfinished tasks;

moved release_results to future.ML; get_some: simplified via Future.release_results;

added release_results (formerly in par_list.ML); more informative trace_active; join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;

Future.release_results;

more tracing;

Theory.checkpoint for main operations, admits concurrent proofs;

promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;

proper transfer of theorems that involve classes being instantiated here;

HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);

eliminated polymorphic equality;

added subset operation;

Added fresh_star_const.

Added some more theorems to NominalData.

Added some more lemmas that are useful in proof of strong induction rule.

removed obsolete name convention "func"

fixed typo

clarified function transformator interface

op = vs. eq

moved future_scheduler flag to skip_proof.ML;

added future_scheduler (from thy_info.ML); prove: Goal.prove_promise if future_schedule;

simplified promise; fulfill is internal only; more robust join_futures;

simplified Thm.promise; prove_common: proper context for promise_result;

explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove; tuned list operations;

explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;

circumvent problem with code redundancy

clarifed redundancy policy

tuned comments;

added release_results; tuned comments;

abtract types: plain datatype with opaque signature matching; promise: join pending futures at end of theory;