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;

documentation is always in PDF;

merged;

clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;

clarified meaning of options for "isabelle options";

more correct context for dynamic invocations of static code conversions etc.

support isabelle options -g;

tuned spelling;

tuned;

standardized aliases;

transfer rule for {c,d}tor_{,un}fold

two useful relation theorems

factored syntactic type classes for bot and top (by Alessandro Coglio)

derive specialized version of full fixpoint induction (with admissibility)

export mono_thm

merged Def_Init_Sound_X into Def_Init_X

proper transfer rule format for map_transfer

merged

eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates

removed obsolete HOL-Boogie session; keep examples that also test SMT solvers, using a minimal version of the old Boogie loader

transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)

separate ML interface to note facts of a bnf

transfer rule for map (not yet registered as a transfer rule)

tuned exercises

clarified option name, with improved sort order wrt. "time" options;

document update at high priority -- important;

option editor_execution_priority;

obscure options;

print_state at high priority -- fast and important;

proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);

old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);

just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);

turned pattern unify flag into configuration option (global only);

merged

permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

added exerciese

do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)

modify background theory where it is actually required (cf. 51dfdcd88e84);

tuned messages -- avoid text folds stemming from Pretty.chunks;

proper system options for 'find_theorems';

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);