2011-02-21 blanchet 2011-02-21 improve optimization
2011-02-21 blanchet 2011-02-21 updated docs
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter
2011-02-21 blanchet 2011-02-21 don't distinguish between "fixes" and other free variables -- this confuses users
2011-02-21 blanchet 2011-02-21 added a timeout around SMT preprocessing (notably monomorphization)
2011-02-21 blanchet 2011-02-21 comments to find fudge factors easily
2011-02-21 boehmes 2011-02-21 added test cases with quantifier occurring in first-order term positions
2011-02-21 boehmes 2011-02-21 wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
2011-02-19 haftmann 2011-02-19 dropped redundancy
2011-02-19 haftmann 2011-02-19 merged
2011-02-17 haftmann 2011-02-17 added is_IAbs; tuned brackets and comments
2011-02-17 haftmann 2011-02-17 more idiomatic printing of let cascades and type variable constraints
2011-02-18 wenzelm 2011-02-18 merged
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2011-02-18 wenzelm 2011-02-18 more precise headers;
2011-02-18 wenzelm 2011-02-18 less verbose tracing;
2011-02-18 wenzelm 2011-02-18 standardized headers;
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2011-02-18 blanchet 2011-02-18 gracious timeout in "blocking" mode
2011-02-18 blanchet 2011-02-18 make Nitpick's timeout mechanism somewhat more reliable/friendly; avoid producing warnings when invoked in "auto" mode
2011-02-18 blanchet 2011-02-18 better fudge factors for Sledgehammer
2011-02-18 blanchet 2011-02-18 adjust fudge factors
2011-02-18 blanchet 2011-02-18 extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
2011-02-17 blanchet 2011-02-17 export more functionality of Sledgehammer to applications (for experiments)
2011-02-16 blanchet 2011-02-16 export useful function (needed in a Sledgehammer-related experiment)
2011-02-15 blanchet 2011-02-15 make experimental "Z3 ATP" work on Linux as well
2011-02-15 blanchet 2011-02-15 adjusted fudge factors (based on Judgment Day runs)
2011-02-14 nipkow 2011-02-14 generalized termination lemmas
2011-02-14 krauss 2011-02-14 strengthened induction rule; clarified some proofs
2011-02-14 boehmes 2011-02-14 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
2011-02-14 boehmes 2011-02-14 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
2011-02-13 wenzelm 2011-02-13 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;
2011-02-13 wenzelm 2011-02-13 eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;
2011-02-13 wenzelm 2011-02-13 tuned;
2011-02-13 nipkow 2011-02-13 more pretty set comprehension sugar
2011-02-11 bulwahn 2011-02-11 merged
2011-02-11 bulwahn 2011-02-11 adjusting HOL-Mutabelle to changes in quickcheck
2011-02-11 bulwahn 2011-02-11 quickcheck can be invoked with its internal timelimit or without
2011-02-11 bulwahn 2011-02-11 quickcheck invokes TimeLimit.timeLimit only in one separate function
2011-02-11 blanchet 2011-02-11 added option to Mirabelle Sledgehammer
2011-02-10 haftmann 2011-02-10 merged
2011-02-10 haftmann 2011-02-10 reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
2011-02-10 blanchet 2011-02-10 tuning
2011-02-10 blanchet 2011-02-10 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)
2011-02-10 blanchet 2011-02-10 fix path to etc/settings and etc/components in doc
2011-02-10 blanchet 2011-02-10 run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
2011-02-10 blanchet 2011-02-10 remove pointless clutter
2011-02-10 blanchet 2011-02-10 make minimizer verbose
2011-02-09 blanchet 2011-02-09 tuning
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09 blanchet 2011-02-09 renamed field
2011-02-09 blanchet 2011-02-09 added "Z3 as an ATP" support to Sledgehammer locally
2011-02-09 blanchet 2011-02-09 remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files
2011-02-09 blanchet 2011-02-09 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
2011-02-09 wenzelm 2011-02-09 tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;
2011-02-09 bulwahn 2011-02-09 merged