always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"

give more weight to Frees than to Consts in relevance filter

don't distinguish between "fixes" and other free variables -- this confuses users

added a timeout around SMT preprocessing (notably monomorphization)

comments to find fudge factors easily

added test cases with quantifier occurring in first-order term positions

wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions

dropped redundancy

merged

added is_IAbs; tuned brackets and comments

more idiomatic printing of let cascades and type variable constraints

merged

modernized specifications;

modernized specifications;

more precise headers;

less verbose tracing;

standardized headers;

modernized specifications;

gracious timeout in "blocking" mode

make Nitpick's timeout mechanism somewhat more reliable/friendly; avoid producing warnings when invoked in "auto" mode

better fudge factors for Sledgehammer

adjust fudge factors

extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs

export more functionality of Sledgehammer to applications (for experiments)

export useful function (needed in a Sledgehammer-related experiment)

make experimental "Z3 ATP" work on Linux as well

adjusted fudge factors (based on Judgment Day runs)

generalized termination lemmas