interruptible: Thread.testInterrupt before changing thread attributes;

wait: absorb spurious interrupts; replaced wait_timeout by explicit wait_interruptible;

scheduler: shutdown spontaneously (after some delay) if queue is empty; scheduler_check: critical, only performed after fork/enqueue; shutdown: passively wait for termination;

join_next: do not yield, even if overloaded, to minimize "running" tasks;

tuned tracing;

cancel: improved reactivity due to more careful broadcasting; internal broadcast_all;

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;

merged

removed unused low-level interrupts;

tuned signature;

tuned;

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;

ML_Context.the_generic_context;

eliminated redundant Library.multiply;

renamed structure Display_Goal to Goal_Display;

tuned tracing;

added Multithreading.real_time;

simplified/unified Multithreading.tracing_time; tuned;

get_name: cover only PThm, not PAxm;

eliminated OldGoals.read_term;

more antiquotations instead of adhoc ML stuff;

ML_Context.the_local_context;

eliminated the_context;

do not open OldGoals;

renamed functor SplitterFun to Splitter, require explicit theory;

renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;

eliminated OldGoals.prove_goal;

explicit OldGoals;

structure OldGoals: no pervasive names;

renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;

renamed functor InductFun to Induct;

tuned;

renamed Pure/tctical.ML to Pure/tactical.ML;

eliminated print_goals_without_context -- proper pretty printing;

Display_Goal.pretty_goals: always Markup.subgoal, clarified options;

removed Formal_Power_Series_Examples (cf. adea7a729c7a);

make: keep going by default;

merged

merged

fixed proof --- fact_setprod removed for fact_altdef_nat

merged

Vandermonde vs Pochhammer; Hypergeometric series - very basic facts

More theorems about pochhammer

Moved theorem binomial_symmetric from Formal_Power_Series to here

Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.

removed obsolete ML proof tools;

more @{theory} antiquotations;

eliminated adhoc ML code;

misc modernization: proper method setup instead of adhoc ML proofs;

global_claset_of;

Proper context for simpset_of, claset_of, clasimpset_of.

local simpset_of;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

merged

paramify_vars: Term_Subst.map_atypsT_same recovered coding conventions of this module;

clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;

use regular Display.string_of_thm_global;

tuned ML_OPTIONS;

fixed doc

Purely functional type inference.

merged

moved complete_lattice &c. into separate theory

merged

tuned proofs and added some lemmas

merged

set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice

set intersection and union now named inter and union

spurious proof failure

original rail implementation by Michael Kerscher;

merged, resolving trivial conflict;

News

explicit antiquotation

merged

merged

obey captialized directory names convention

dropped ancient flat_names option

dropped ancient flat_names option

integrated add_triv_classes into evaluation stack

more accurate check of judgment type

UNIV_code now named UNIV_apply

attempt for more concise setup of non-etacontracting binders

moved abstract algebra section to the end

merged

Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy

merged

swapped bootstrap order of UNION/Union and INTER/Inter in theory Set

merged

dropped add_registration interface in locale

Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM

Tests for executability of "prime"