| Thu, 29 Jul 2010 17:45:22 +0200 |
work around atomization failures
|
file | diff | annotate |
| Thu, 29 Jul 2010 16:41:32 +0200 |
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
|
file | diff | annotate |
| Thu, 29 Jul 2010 16:11:02 +0200 |
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
|
file | diff | annotate |
| Thu, 29 Jul 2010 15:50:26 +0200 |
generate correct names for "$true" and "$false";
|
file | diff | annotate |
| Thu, 29 Jul 2010 15:37:27 +0200 |
don't assume canonical rule format
|
file | diff | annotate |
| Thu, 29 Jul 2010 14:53:55 +0200 |
avoid "clause" and "cnf" terminology where it no longer makes sense
|
file | diff | annotate |
| Thu, 29 Jul 2010 14:42:09 +0200 |
"axiom_clauses" -> "axioms" (these are no longer clauses)
|
file | diff | annotate |
| Thu, 29 Jul 2010 14:39:43 +0200 |
remove the "extra_clauses" business introduced in 19a5f1c8a844;
|
file | diff | annotate |
| Wed, 28 Jul 2010 23:01:27 +0200 |
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
|
file | diff | annotate |
| Wed, 28 Jul 2010 18:54:18 +0200 |
minor refactoring
|
file | diff | annotate |
| Wed, 28 Jul 2010 18:07:25 +0200 |
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
|
file | diff | annotate |
| Wed, 28 Jul 2010 17:38:40 +0200 |
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
|
file | diff | annotate |
| Wed, 28 Jul 2010 10:45:49 +0200 |
renaming
|
file | diff | annotate |
| Wed, 28 Jul 2010 00:53:24 +0200 |
improve detection of installed SPASS
|
file | diff | annotate |
| Tue, 27 Jul 2010 19:41:19 +0200 |
minor refactoring
|
file | diff | annotate |
| Tue, 27 Jul 2010 18:33:10 +0200 |
more refactoring
|
file | diff | annotate |
| Tue, 27 Jul 2010 17:56:01 +0200 |
rename "ATP_Manager" ML module to "Sledgehammer";
|
file | diff | annotate |
| Tue, 27 Jul 2010 17:49:16 +0200 |
rename
|
file | diff | annotate | base |