blanchet [Fri, 18 Feb 2011 15:17:39 +0100] rev 41770
adjust fudge factors
blanchet [Fri, 18 Feb 2011 12:32:55 +0100] rev 41769
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet [Thu, 17 Feb 2011 12:14:47 +0100] rev 41768
export more functionality of Sledgehammer to applications (for experiments)
blanchet [Wed, 16 Feb 2011 19:07:53 +0100] rev 41767
export useful function (needed in a Sledgehammer-related experiment)
blanchet [Tue, 15 Feb 2011 18:32:58 +0100] rev 41766
make experimental "Z3 ATP" work on Linux as well
blanchet [Tue, 15 Feb 2011 10:03:10 +0100] rev 41765
adjusted fudge factors (based on Judgment Day runs)
nipkow [Mon, 14 Feb 2011 18:28:36 +0100] rev 41764
generalized termination lemmas
krauss [Mon, 14 Feb 2011 15:27:23 +0100] rev 41763
strengthened induction rule;
clarified some proofs
boehmes [Mon, 14 Feb 2011 12:25:26 +0100] rev 41762
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
boehmes [Mon, 14 Feb 2011 10:40:43 +0100] rev 41761
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