renamed structure TaskQueue to Task_Queue;

renamed structure TaskQueue to Task_Queue; generalized fork_background to fork_pri; reduced tracing; map: inherit task priority; removed unused focus;

removed old scheduler;

tuned enqueue: plain add_edge, acyclic not required here;

tuned messages;

updated generated file;

repaired railroad accident;

updated generated files;

added 'atp_messages' command, which displays recent messages synchronously;

merged

flipped fold implementation

merged

codegen

code for {x:A. P(x)} and for fold

Testfile for Stefan's code generator

moved value.ML to src/Tools

\underscoreoff is now default

tuned some proofs

removed Ids;

merged

merged

merged

Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.

Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.

merged

tuned comments; tuned;

tuned ML_OPTIONS for improved multicore performance;

refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;

requires: check ancestors directly;

Context.display_names;

global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;

usage: echo ML settings as well;

future proofs: more robust check via Future.enabled;

removed former Isabelle font (cf. IsabelleItalic);

incorporated isabelle-fonts side-branch (forced merge);

replaced single quote by mathematical prime;

generated file;

bold version: math glyphs from plain IsabelleMono;

fixed rangle;

use dash from text font, not math;

added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak); replaced old-style digits by bold ones (bf);

generated ttf;

renamed to IsabelleMono;

added README with original licenses;

renamed Isabelle to IsabelleItalic;

fixed rangle glyph;

the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;

Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);

Isabelle font, based on TeX glyhps;

enable future_scheduler by default;

ISABELLE_USEDIR_OPTIONS: -M max is default;

unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;

removed spurious exception_trace;

print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);