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;

attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead

tuned variable names

got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)

some new lemmas towards getting rid of in_bd BNF property; tuned

tuned

added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases

merged

more robust proof export / import due to Stefan Berghofer; eliminated musing in the manual that is not quite right;

added blast, force

removed |>! and #>!

tuned * * * easier debugging * * * tuned

cleaner preplay interface

tuned;

tuned proofs;

updated keywords;

localized and modernized adhoc-overloading (patch by Christian Sternagel);

merged

tuned proof;

reraise interrupts outside command regular transactions -- relevant for memo_stable;

added "isabelle update_sub_sup" tool;

allow spaces in file names; tuned;

more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;

added |>! and #>! for convenient printing of timing information

preplay failures might be resolved later, so proceed as usual

more reasonable preplay_interface semantics

tuned

minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps

merged

clarified memo_exec: plain synchronized access without any special tricks;

tuned;

clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;

tuned signature; tuned comments;

clarified module name;

more explicit type Exec.context; eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;