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;

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;