| Fri, 18 Feb 2011 15:17:39 +0100 |
blanchet |
adjust fudge factors
|
changeset |
files
|
| Fri, 18 Feb 2011 12:32:55 +0100 |
blanchet |
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
|
changeset |
files
|
| Thu, 17 Feb 2011 12:14:47 +0100 |
blanchet |
export more functionality of Sledgehammer to applications (for experiments)
|
changeset |
files
|
| Wed, 16 Feb 2011 19:07:53 +0100 |
blanchet |
export useful function (needed in a Sledgehammer-related experiment)
|
changeset |
files
|
| Tue, 15 Feb 2011 18:32:58 +0100 |
blanchet |
make experimental "Z3 ATP" work on Linux as well
|
changeset |
files
|
| Tue, 15 Feb 2011 10:03:10 +0100 |
blanchet |
adjusted fudge factors (based on Judgment Day runs)
|
changeset |
files
|
| Mon, 14 Feb 2011 18:28:36 +0100 |
nipkow |
generalized termination lemmas
|
changeset |
files
|
| Mon, 14 Feb 2011 15:27:23 +0100 |
krauss |
strengthened induction rule;
|
changeset |
files
|
| Mon, 14 Feb 2011 12:25:26 +0100 |
boehmes |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
changeset |
files
|
| Mon, 14 Feb 2011 10:40:43 +0100 |
boehmes |
more explicit errors to inform users about problems related to SMT solvers;
|
changeset |
files
|
| Sun, 13 Feb 2011 17:45:21 +0100 |
wenzelm |
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;
|
changeset |
files
|
| Sun, 13 Feb 2011 17:29:44 +0100 |
wenzelm |
eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;
|
changeset |
files
|