2009-07-27 ago wenzelm moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-27 ago wenzelm interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-27 ago wenzelm wait: absorb spurious interrupts;
2009-07-27 ago wenzelm scheduler: shutdown spontaneously (after some delay) if queue is empty;
2009-07-27 ago wenzelm join_next: do not yield, even if overloaded, to minimize "running" tasks;
2009-07-27 ago wenzelm tuned tracing;
2009-07-27 ago wenzelm cancel: improved reactivity due to more careful broadcasting;
2009-07-27 ago wenzelm dequeue_towards: always return active tasks;
2009-07-27 ago wenzelm merged
2009-07-27 ago wenzelm removed unused low-level interrupts;
2009-07-27 ago wenzelm tuned signature;
2009-07-27 ago wenzelm tuned;
2009-07-27 ago wenzelm more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
2009-07-27 ago wenzelm enqueue/finish: return minimal/maximal state of this task;
2009-07-27 ago haftmann NEWS
2009-07-26 ago wenzelm tacticals FOCUS and FOCUS_PARAMS;
2009-07-26 ago wenzelm replaced old METAHYPS by FOCUS;
2009-07-26 ago wenzelm replaced old METAHYPS by FOCUS;
2009-07-26 ago wenzelm added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
2009-07-26 ago wenzelm replaced old METAHYPS by FOCUS;
2009-07-26 ago wenzelm tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
2009-07-26 ago wenzelm retrofit: actually handle schematic variables -- need to export into original context;
2009-07-26 ago wenzelm merged
2009-07-26 ago haftmann adapted to changed prefixes
2009-07-26 ago haftmann merged
2009-07-25 ago haftmann improved handling of parameter import; tuned
2009-07-25 ago haftmann explicit is better than implicit
2009-07-25 ago haftmann localized interpretation of min/max-lattice
2009-07-25 ago haftmann adapted to localized interpretation of min/max-lattice
2009-07-26 ago wenzelm SUBPROOF/Obtain.result: named params;
2009-07-26 ago wenzelm updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
2009-07-26 ago wenzelm advanced retrofit, which allows new subgoals and variables;
2009-07-26 ago wenzelm Variable.focus: named parameters;
2009-07-26 ago wenzelm lambda/cabs/all: named variants;
2009-07-26 ago wenzelm Goal.finish: explicit context for printing;
2009-07-25 ago wenzelm fixed Method.Basic;
2009-07-25 ago wenzelm eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;
2009-07-25 ago wenzelm Method.Basic: no position;
2009-07-25 ago wenzelm basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
2009-07-25 ago wenzelm dequeue_towards: need to try imm_preds as well;
2009-07-25 ago wenzelm internal session timing;
2009-07-25 ago wenzelm enqueue: maintain transitive closure, which simplifies dequeue_towards;
2009-07-25 ago wenzelm ML_Context.the_generic_context;
2009-07-25 ago wenzelm eliminated redundant Library.multiply;
2009-07-25 ago wenzelm renamed structure Display_Goal to Goal_Display;
2009-07-25 ago wenzelm tuned tracing;
2009-07-25 ago wenzelm added Multithreading.real_time;
2009-07-25 ago wenzelm simplified/unified Multithreading.tracing_time;
2009-07-24 ago wenzelm get_name: cover only PThm, not PAxm;
2009-07-24 ago wenzelm eliminated OldGoals.read_term;
2009-07-24 ago wenzelm more antiquotations instead of adhoc ML stuff;
2009-07-24 ago wenzelm ML_Context.the_local_context;
2009-07-24 ago wenzelm eliminated the_context;
2009-07-24 ago wenzelm do not open OldGoals;
2009-07-24 ago wenzelm renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-24 ago wenzelm renamed functor BlastFun to Blast, require explicit theory;
2009-07-24 ago wenzelm eliminated OldGoals.prove_goal;
2009-07-24 ago wenzelm explicit OldGoals;
2009-07-24 ago wenzelm structure OldGoals: no pervasive names;
2009-07-24 ago wenzelm renamed functor ProjectRuleFun to Project_Rule;