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

strengthened induction rule; clarified some proofs

limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate

more explicit errors to inform users about problems related to SMT solvers; fall back to remote SMT solver (if local version does not exist); extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18

more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;

eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;

tuned;

more pretty set comprehension sugar

merged

adjusting HOL-Mutabelle to changes in quickcheck

quickcheck can be invoked with its internal timelimit or without

quickcheck invokes TimeLimit.timeLimit only in one separate function

added option to Mirabelle Sledgehammer

merged

reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space

tuning

fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)

fix path to etc/settings and etc/components in doc

run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user

remove pointless clutter

make minimizer verbose

tuning

automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)

renamed field

added "Z3 as an ATP" support to Sledgehammer locally

remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files

added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation

tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;

merged

changing auto-quickcheck to be considered a non-interactive invocation of quickcheck

discontinued obsolete lib/scripts/polyml-platform;

clarified comment -- ancienct PG 3.7.x is still in use;

discontinued obsolete alias HOL.thy for @{theory HOL} in ML;

prefer polyml-5.2.1 over odd polyml-5.3.0-old;

some shuffling of isatest settings, to ensure coverage of polyml-5.2.1, polyml-5.3.0, polyml-5.4.0, polyml-5.4.1 (SVN), smlnj/110.72;