| Tue, 22 Jun 2010 23:54:02 +0200 |
blanchet |
factor out TPTP format output into file of its own, to facilitate further changes
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 10:36:01 +0200 |
blanchet |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:10:23 +0200 |
blanchet |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 09:36:45 +0200 |
blanchet |
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 14:40:36 +0200 |
blanchet |
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:06:41 +0200 |
blanchet |
renamed module "ATP_Wrapper" to "ATP_Systems"
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 17:38:25 +0200 |
blanchet |
move the minimizer to the Sledgehammer directory
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 19:49:57 +0200 |
blanchet |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:31:37 +0100 |
blanchet |
add new file "sledgehammer_util.ML" to setup
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:33:18 +0100 |
blanchet |
move all ATP setup code into ATP_Wrapper
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:37:44 +0100 |
blanchet |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file |
diff |
annotate
| base
|