guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;

provide global operations as well;

tuned signature;

tuned;

explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;

immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;

merged

tuned message;

tuned signature;

tuned

merged

more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);

tuned spelling;

show variants in error messages; more precise error messages (give witnesses for multiple instances)

refactoring

more robust exn_messages_ids; more robust failure of exn_messages_ids;

non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);

take context from static theory, not dynamic theory certificate;

more official Thm.eq_thm_strict, without demanding ML equality type;

tuned;

tuned definition of seqseq; clarified usage of diagseq via diagseq_holds

merged

Cygwin with Latex according to Cygwin-Latex-Setup.bat (presently unused);

overwrite target;

fully-automated packaging (requires Mac OS X);

more robust application init;

more self-contained application, with side-entry for init;

dispose intermediate 7z archive;

prefer stand-alone javaw;

more robust executable path specifications; afford final test of Isabelle.init; tuned;

separate module XZ_File to avoid initial dependency on org.tukaani.xz;

build Windows application on the spot, using Unix tools;

recover Cygwin symlinks via Windows file-system operations;

produce 7z archive for windows and preserve symlinks separately;

Scala version of init.bat;

tuned line length;

prefer @{file} references that are actually checked;

deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";

retain compile-time context visibility, which is particularly important for "apply tactic";

use transfer/lifting for proving countable set and multisets being BNFs

added exercise

killed unused theorems

eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)

tuned specifications and proofs;

tuned;

keep persistent prints only if actually finished;

more careful termination of removed execs, leaving running execs undisturbed;

recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;

merged

avoid spurious warnings, notably of 'try0' about already declared simps etc.;

initial delay for automatically tried tools;

more rendering for information messages;

update_options with full update, e.g. required for re-assignment of Command.prints;

tuned;

determine print function parameters dynamically, e.g. depending on runtime options;

NEWS;

clarified some default options;

gutter icon for information messages; avoid redundant Pretty.chunks to keep Markup.information node topmost;

more explicit Markup.information for messages produced by "auto" tools;

full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

compile

system options for Isabelle/HOL proof tools;

removed unused Predicate_Compile component setup;