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
|
Sun, 13 Feb 2011 17:19:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 13 Feb 2011 08:47:36 +0100 |
nipkow |
more pretty set comprehension sugar
|
changeset |
files
|
Fri, 11 Feb 2011 15:31:19 +0100 |
bulwahn |
merged
|
changeset |
files
|
Fri, 11 Feb 2011 11:47:44 +0100 |
bulwahn |
adjusting HOL-Mutabelle to changes in quickcheck
|
changeset |
files
|
Fri, 11 Feb 2011 11:47:43 +0100 |
bulwahn |
quickcheck can be invoked with its internal timelimit or without
|
changeset |
files
|
Fri, 11 Feb 2011 11:47:42 +0100 |
bulwahn |
quickcheck invokes TimeLimit.timeLimit only in one separate function
|
changeset |
files
|
Fri, 11 Feb 2011 11:54:24 +0100 |
blanchet |
added option to Mirabelle Sledgehammer
|
changeset |
files
|
Thu, 10 Feb 2011 18:44:39 +0100 |
haftmann |
merged
|
changeset |
files
|
Thu, 10 Feb 2011 10:32:12 +0100 |
haftmann |
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
|
changeset |
files
|