pro-forma Goal.reset_futures, despite lack of final join/commit;

tuned;

tuned;

back to model.update_perspective with delay (cf. a20631db9c8a);

show displaced messages (e.g. from protocol thread) as raw output;

actually purge removed goal futures -- avoid memory leak;

tuned -- less redundant data structure;

always init GUI state;

tuned signature;

discontinued notion of "stable" result -- running execution is never canceled;

obsolete;

support declarative editor_execution_range, instead of old-style check/cancel buttons;

avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference

updated Sledgehammer prover versions

parse nonnumeric identifiers in E proofs correctly

simplified Vampire hack -- no need to run it for other ATPs

added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")

prefer examples that work out of the box;

breakable @{file};

prefer existing swipl;

avoid machine running batch process for months;

more converse(p) theorems; tuned proofs;

more uniform cleanup;

tuned;

discontinued historic document formats;

avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;

tuned;

discontinued ISABELLE_DOC_FORMAT;

more direct inclusion of tikz pictures;

obsolete;