prefer Isabelle/ML concurrency elements; more careful propagation of interrupts;

removed bash from ML system bootstrap, and past the Secure ML barrier;

more proper int wrappers;

explicit check for requirement;

more basic Isabelle_System.mkdir;

tuned;

more explicit Isabelle_System operations;

prefer Synchronized.var over CRITICAL/Unsynchronized.ref;

moved file identification to thy_load.ML (where it is actually used);

removed some old settings;

recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);

merged

remove map function names from domain package theory data

isar-style proof for lemma contI2

remove case combinator for fixrec match type

declare more simp rules for powerdomains

merged; adapted ListPair.UnequalLengths;

merged

strict forall2

nbe decides equality of abstractions by extensionality

eliminated some generated comments;

merged

merged

keep type variable arguments of datatype constructors in bookkeeping

document changes in Nitpick and MESON/Metis

renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

just one version of fold_rev2;

explicit use of unprefix;