2009-07-29 haftmann 2009-07-29 abstractions: desymbolize name hint
2009-07-29 haftmann 2009-07-29 added numeral code postprocessor rules on type int
2009-07-29 nipkow 2009-07-29 sos comments modified
2009-07-29 nipkow 2009-07-29 sos documentation
2009-07-29 nipkow 2009-07-29 Added remote-SOS changes by Philipp Meyer
2009-07-24 Philipp Meyer 2009-07-24 Functionality for sum of squares to call a remote csdp prover
2009-07-28 wenzelm 2009-07-28 merged
2009-07-28 haftmann 2009-07-28 updated generated document
2009-07-28 haftmann 2009-07-28 reinserted legacy ML function
2009-07-28 haftmann 2009-07-28 Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-07-28 haftmann 2009-07-28 explicit is better than implicit
2009-07-29 wenzelm 2009-07-29 Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;
2009-07-29 wenzelm 2009-07-29 removed old global get_claset/map_claset; added local get_claset/put_claset;
2009-07-28 wenzelm 2009-07-28 eliminated METAHYPS;
2009-07-28 wenzelm 2009-07-28 Future.shutdown before loading sequentially -- workaround scheduler deadlock;
2009-07-28 wenzelm 2009-07-28 ResAxioms.neg_conjecture_clauses: proper context; let exceptions get through unhindered -- Poly/ML exception_trace will do the tracing;
2009-07-28 wenzelm 2009-07-28 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning;
2009-07-28 wenzelm 2009-07-28 Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
2009-07-28 wenzelm 2009-07-28 eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-28 wenzelm 2009-07-28 non-critical use_thy;
2009-07-28 wenzelm 2009-07-28 future result: Synchronized.var;
2009-07-28 wenzelm 2009-07-28 added unsynchronized Synchronized.peek;
2009-07-28 wenzelm 2009-07-28 group status: Synchronized.var;
2009-07-28 wenzelm 2009-07-28 tuned;
2009-07-28 wenzelm 2009-07-28 Task_Queue.dequeue: explicit thread;
2009-07-28 wenzelm 2009-07-28 more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
2009-07-28 wenzelm 2009-07-28 interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
2009-07-28 wenzelm 2009-07-28 misc tuning;
2009-07-28 krauss 2009-07-28 tuned
2009-07-28 krauss 2009-07-28 moved obsolete same_fst to Recdef.thy
2009-07-28 krauss 2009-07-28 adapted doc to type of "op O"
2009-07-28 wenzelm 2009-07-28 merged
2009-07-27 wenzelm 2009-07-27 merged
2009-07-27 wenzelm 2009-07-27 merged
2009-07-27 wenzelm 2009-07-27 merged
2009-07-27 krauss 2009-07-27 added proof of Kleene_Algebra.star_decomp
2009-07-27 krauss 2009-07-27 added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
2009-07-27 krauss 2009-07-27 some lemmas about maps (contributed by Peter Lammich)
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;