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;

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;

tuned signature; unified exceptions for this module;

strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;

tuned -- cleanup before publishing assignment;

more abstract types; tuned signature;

tuned;

disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution; tuned error messages: prefer plain "error" as in document.ML;

more precise fact declarations -- fewer warnings;

global management of command execution fragments; tuned;

fully synchronized guard of running execution; tuned;

merged

added exercises

optimize isar-proofs by trying different proof methods

made SML/NJ happy

tuned

tuned;

re-assign prints of unchanged eval only -- avoid crash of new_exec;

tuned -- refrain from odd optimization;

tuned;

added "echo" command for demonstration purposes;

more abstract message channel;

explicit shutdown of message output thread;

tuned signature;

no need for raw stdin;

fall back on synchronous message output for single-threaded SML/NJ;

make SML/NJ happy;

retain main thread for protocol loop -- no access to raw ML toplevel;

removed historic dimacs2hol (see also read_dimacs_cnf_file in src/HOL/Tools/sat_solver.ML);

less intrusive token_range rendering, which is relevant for inner parse errors;

made SML/NJ happy

merged

tuned start_execution: avoid sleep on worker thread;

print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;

allow to remove print functions; tuned signature;

clarified Command.print: update old prints here;

produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);

tuned;

tuned proofs;

more formal type assign_update: avoid duplicate results and redundant update of global State.execs;

tuned message;

tuned signature -- NB: Command.read is actually part of Command.eval;

tuned protocol terminology; tuned signature;

tuned;

allow whitespace in file names;

tuned;

more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;

allow worker guest threads, which participate actively in future joins, but are outside thread accounting;