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;

prove: error with original thread position;

explicit type OrdList.T;

(temporary workaround)

(temporal deactivation)

non left-linear equations for nbe

non left-linear equations for nbe

map_force

matchess

burrow_fst

discontinued special treatment of op = vs. eq_class.eq

report: produce individual status messages;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy); added Kind.code map;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);

init: OuterKeyword.report;

prove_multi: immediate;

added promise_result, prove_promise;

Corrected call of SUBPROOF in coherent_tac that used wrong context.