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

document requirement on theory import

corrected abd4e7358847 where SOMEthing went utterly wrong

merged

swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)

instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers

removing Enum.in_enum from the claset

merged

be more precise: only treat constant 'distinct' applied to an explicit list as built-in

be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

announcing some latest change (d40b347d5b0b)

merged

more precise characterization of built-in constants "number_of", "0", and "1"

merged

merged

adhere established Collect/mem convention more closely

merged

replaced misleading Fset/fset name -- these do not stand for finite sets

renamed slightly ambivalent crel to effect

disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day

more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT

use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on

make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT

try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates

added "verbose" option to Metis to shut up its warnings if necessary

added support for quantifier weight annotations

share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'

added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions