| Wed, 28 Jul 2010 19:04:59 +0200 |
consequence of directory renaming
|
file | diff | annotate |
| Tue, 27 Jul 2010 19:41:19 +0200 |
minor refactoring
|
file | diff | annotate |
| Tue, 27 Jul 2010 19:17:15 +0200 |
standardize "Author" tags
|
file | diff | annotate |
| Tue, 27 Jul 2010 18:45:55 +0200 |
reorder ML files in theory
|
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:43:11 +0200 |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file | diff | annotate |
| Mon, 28 Jun 2010 18:47:07 +0200 |
no setup is necessary anymore
|
file | diff | annotate |
| Fri, 25 Jun 2010 18:05:36 +0200 |
factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
|
file | diff | annotate |
| Fri, 25 Jun 2010 17:13:38 +0200 |
reorder ML files
|
file | diff | annotate |
| Fri, 25 Jun 2010 17:08:39 +0200 |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
|
file | diff | annotate |
| Fri, 25 Jun 2010 16:42:06 +0200 |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file | diff | annotate |
| Fri, 25 Jun 2010 16:15:03 +0200 |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file | diff | annotate |
| Fri, 25 Jun 2010 15:30:38 +0200 |
more moving around of ML files in "Sledgehammer.thy"
|
file | diff | annotate |
| Fri, 25 Jun 2010 15:18:58 +0200 |
move "MESON" up;
|
file | diff | annotate |
| Thu, 24 Jun 2010 17:57:36 +0200 |
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
|
file | diff | annotate |
| Wed, 23 Jun 2010 09:40:06 +0200 |
killed legacy "neg_clausify" and "clausify"
|
file | diff | annotate |
| Tue, 22 Jun 2010 23:54:02 +0200 |
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 |
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 |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file | diff | annotate |
| Fri, 30 Apr 2010 09:36:45 +0200 |
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 |
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
|
file | diff | annotate |
| Fri, 23 Apr 2010 18:11:41 +0200 |
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 |
renamed module "ATP_Wrapper" to "ATP_Systems"
|
file | diff | annotate |
| Fri, 23 Apr 2010 17:38:25 +0200 |
move the minimizer to the Sledgehammer directory
|
file | diff | annotate |
| Mon, 29 Mar 2010 19:49:57 +0200 |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file | diff | annotate |
| Mon, 29 Mar 2010 15:50:18 +0200 |
get rid of Polyhash, since it's no longer used
|
file | diff | annotate |
| Wed, 24 Mar 2010 12:31:37 +0100 |
add new file "sledgehammer_util.ML" to setup
|
file | diff | annotate |
| Fri, 19 Mar 2010 15:33:18 +0100 |
move all ATP setup code into ATP_Wrapper
|
file | diff | annotate |
| Fri, 19 Mar 2010 15:07:44 +0100 |
move the Sledgehammer Isar commands together into one file;
|
file | diff | annotate |
| Fri, 19 Mar 2010 13:02:18 +0100 |
more Sledgehammer refactoring
|
file | diff | annotate |
| Wed, 17 Mar 2010 19:37:44 +0100 |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file | diff | annotate | base |