| Wed, 02 Jan 2013 13:50:59 +0100 |
wenzelm |
inline ML statistics into build log;
|
changeset |
files
|
| Wed, 02 Jan 2013 13:20:10 +0100 |
wenzelm |
removed outdated comment;
|
changeset |
files
|
| Wed, 02 Jan 2013 13:06:54 +0100 |
wenzelm |
enable Z3 for full test (cf. 6f48853f08d5);
|
changeset |
files
|
| Wed, 02 Jan 2013 20:53:01 +0100 |
smolkas |
removed old, unused code
|
changeset |
files
|
| Wed, 02 Jan 2013 20:52:39 +0100 |
smolkas |
removed whitespace
|
changeset |
files
|
| Wed, 02 Jan 2013 20:52:32 +0100 |
smolkas |
removed duplicate code
|
changeset |
files
|
| Wed, 02 Jan 2013 20:35:49 +0100 |
smolkas |
use rpair to avoid swap
|
changeset |
files
|
| Wed, 02 Jan 2013 19:59:06 +0100 |
blanchet |
generate "obtain" steps corresponding to skolemization inferences
|
changeset |
files
|
| Wed, 02 Jan 2013 16:32:40 +0100 |
blanchet |
keep E's and Vampire's skolemization steps
|
changeset |
files
|
| Wed, 02 Jan 2013 16:02:33 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 02 Jan 2013 15:54:38 +0100 |
blanchet |
fixed oversensitive Skolem handling (cf. eaa540986291)
|
changeset |
files
|
| Wed, 02 Jan 2013 15:44:00 +0100 |
blanchet |
added "obtain" to Isar proof construction data structure
|
changeset |
files
|
| Wed, 02 Jan 2013 13:31:13 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 02 Jan 2013 13:14:47 +0100 |
blanchet |
properly take the existential closure of skolems
|
changeset |
files
|
| Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
changeset |
files
|