2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-28 wenzelm 2009-07-28 added rail antiquotation environment, which coexists with old-style content markup;
2009-07-28 wenzelm 2009-07-28 proper header; proper structure; tuned white space;
2009-07-27 wenzelm 2009-07-27 proper context for SAT tactics; eliminated METAHYPS; tuned signatures;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-07-27 wenzelm 2009-07-27 interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-27 wenzelm 2009-07-27 wait: absorb spurious interrupts; replaced wait_timeout by explicit wait_interruptible;
2009-07-27 wenzelm 2009-07-27 scheduler: shutdown spontaneously (after some delay) if queue is empty; scheduler_check: critical, only performed after fork/enqueue; shutdown: passively wait for termination;
2009-07-27 wenzelm 2009-07-27 join_next: do not yield, even if overloaded, to minimize "running" tasks;
2009-07-27 wenzelm 2009-07-27 tuned tracing;
2009-07-27 wenzelm 2009-07-27 cancel: improved reactivity due to more careful broadcasting; internal broadcast_all;
2009-07-27 wenzelm 2009-07-27 dequeue_towards: always return active tasks; join_work: imitate worker more closely, keep active if queue appears to be blocked for the moment -- it may become free again after some worker_finished event;
2009-07-27 wenzelm 2009-07-27 merged
2009-07-27 wenzelm 2009-07-27 removed unused low-level interrupts;
2009-07-27 wenzelm 2009-07-27 tuned signature;
2009-07-27 wenzelm 2009-07-27 tuned;
2009-07-27 wenzelm 2009-07-27 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;
2009-07-27 wenzelm 2009-07-27 enqueue/finish: return minimal/maximal state of this task;
2009-07-27 haftmann 2009-07-27 NEWS
2009-07-26 wenzelm 2009-07-26 tacticals FOCUS and FOCUS_PARAMS;
2009-07-26 wenzelm 2009-07-26 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?);
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-07-26 wenzelm 2009-07-26 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-07-26 wenzelm 2009-07-26 tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
2009-07-26 wenzelm 2009-07-26 retrofit: actually handle schematic variables -- need to export into original context;
2009-07-26 wenzelm 2009-07-26 merged
2009-07-26 haftmann 2009-07-26 adapted to changed prefixes
2009-07-26 haftmann 2009-07-26 merged
2009-07-25 haftmann 2009-07-25 improved handling of parameter import; tuned
2009-07-25 haftmann 2009-07-25 explicit is better than implicit
2009-07-25 haftmann 2009-07-25 localized interpretation of min/max-lattice
2009-07-25 haftmann 2009-07-25 adapted to localized interpretation of min/max-lattice
2009-07-26 wenzelm 2009-07-26 SUBPROOF/Obtain.result: named params;
2009-07-26 wenzelm 2009-07-26 updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
2009-07-26 wenzelm 2009-07-26 advanced retrofit, which allows new subgoals and variables; added FOCUS -- does not require closed proof;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-26 wenzelm 2009-07-26 lambda/cabs/all: named variants;
2009-07-26 wenzelm 2009-07-26 Goal.finish: explicit context for printing;
2009-07-25 wenzelm 2009-07-25 fixed Method.Basic;
2009-07-25 wenzelm 2009-07-25 eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;
2009-07-25 wenzelm 2009-07-25 Method.Basic: no position;
2009-07-25 wenzelm 2009-07-25 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;
2009-07-25 wenzelm 2009-07-25 dequeue_towards: need to try imm_preds as well;
2009-07-25 wenzelm 2009-07-25 internal session timing;
2009-07-25 wenzelm 2009-07-25 enqueue: maintain transitive closure, which simplifies dequeue_towards;
2009-07-25 wenzelm 2009-07-25 ML_Context.the_generic_context;
2009-07-25 wenzelm 2009-07-25 eliminated redundant Library.multiply;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-25 wenzelm 2009-07-25 tuned tracing;
2009-07-25 wenzelm 2009-07-25 added Multithreading.real_time;
2009-07-25 wenzelm 2009-07-25 simplified/unified Multithreading.tracing_time; tuned;
2009-07-24 wenzelm 2009-07-24 get_name: cover only PThm, not PAxm;
2009-07-24 wenzelm 2009-07-24 eliminated OldGoals.read_term;
2009-07-24 wenzelm 2009-07-24 more antiquotations instead of adhoc ML stuff;
2009-07-24 wenzelm 2009-07-24 ML_Context.the_local_context;
2009-07-24 wenzelm 2009-07-24 eliminated the_context;
2009-07-24 wenzelm 2009-07-24 do not open OldGoals;
2009-07-24 wenzelm 2009-07-24 renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;