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;

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

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;