Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;

non-critical use_thy;

future result: Synchronized.var;

added unsynchronized Synchronized.peek;

group status: Synchronized.var;

tuned;

Task_Queue.dequeue: explicit thread;

more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;

interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);

misc tuning;

tuned

moved obsolete same_fst to Recdef.thy

adapted doc to type of "op O"

merged

merged

merged

merged

added proof of Kleene_Algebra.star_decomp

added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)

some lemmas about maps (contributed by Peter Lammich)

"more standard" argument order of relation composition (op O)

added rail antiquotation environment, which coexists with old-style content markup;

proper header; proper structure; tuned white space;

proper context for SAT tactics; eliminated METAHYPS; tuned signatures;

moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);

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