more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads; more specific signal vs. broadcast; execute/finish: more careful notification based on minimal/maximal status; tuned shutdown;

enqueue/finish: return minimal/maximal state of this task;

NEWS

tacticals FOCUS and FOCUS_PARAMS;

replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);

replaced old METAHYPS by FOCUS;

added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;

replaced old METAHYPS by FOCUS;

tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);

retrofit: actually handle schematic variables -- need to export into original context;

merged

adapted to changed prefixes

merged

improved handling of parameter import; tuned

explicit is better than implicit

localized interpretation of min/max-lattice

adapted to localized interpretation of min/max-lattice

SUBPROOF/Obtain.result: named params;

updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;

advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;

Variable.focus: named parameters;

lambda/cabs/all: named variants;

Goal.finish: explicit context for printing;

fixed Method.Basic;

eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;

Method.Basic: no position;

basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;

dequeue_towards: need to try imm_preds as well;

internal session timing;

enqueue: maintain transitive closure, which simplifies dequeue_towards;