added evaluation section

tuned formatting; adjustments to changes on ML level

added label

more thorough process termination (cf. Scala version);

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;

keep private things private, without comments;

eliminated some clones of eq_list;

merged

new lemma

lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

prefer non-classical eliminations in Pure reasoning, notably "rule" steps;

discontinued global "Isabelle" symlink, to make each distribution even more self-contained;

more correct spelling;

globbing constant expressions use more idiomatic underscore rather than star

globbing constant expressions use more idiomatic underscore rather than star; precised

datatype constructor glob for code_reflect

merged

merged

merged

toplevel deresolving for flat module name space

merged

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

Replace surj by abbreviation; remove surj_on.

adjust Sledgehammer/SMT fudge factor

clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);

merge

cosmetics

eta-reduce on the fly to prevent an exception

merged

Added the simplest finite Ramsey theorem

reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions

set Metis option on correct context, lest it be ignored

make "debug" mode of Sledgehammer/SMT more liberal

fix check for builtinness of 0 and 1 -- these aren't functions

added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway