| Tue, 07 Jun 2011 07:06:24 +0200 |
blanchet |
renamed ML function
|
changeset |
files
|
| Tue, 07 Jun 2011 07:04:53 +0200 |
blanchet |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
changeset |
files
|
| Tue, 07 Jun 2011 06:58:52 +0200 |
blanchet |
pass props not thms to ATP translator
|
changeset |
files
|
| Mon, 06 Jun 2011 23:46:02 +0200 |
blanchet |
slighly more reasonable Vampire slices (until new monomorphizer is used)
|
changeset |
files
|
| Mon, 06 Jun 2011 23:43:28 +0200 |
blanchet |
removed confusing slicing logic
|
changeset |
files
|
| Mon, 06 Jun 2011 23:26:40 +0200 |
blanchet |
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
|
changeset |
files
|
| Mon, 06 Jun 2011 23:11:14 +0200 |
blanchet |
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
|
changeset |
files
|
| Mon, 06 Jun 2011 22:03:58 +0200 |
blanchet |
minor: curly brackets, not square brackets
|
changeset |
files
|
| Mon, 06 Jun 2011 21:58:29 +0200 |
blanchet |
document metis better in Sledgehammer docs
|
changeset |
files
|
| Mon, 06 Jun 2011 21:02:24 +0200 |
blanchet |
updated Sledgehammer message
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
removed old optimization that isn't one anyone
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
generate less type information in polymorphic case
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:36 +0200 |
blanchet |
enable new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
made "explicit_apply"'s smart mode (more) complete
|
changeset |
files
|