src/HOL/Tools/Sledgehammer/sledgehammer.ML
Mon, 09 Aug 2010 14:08:30 +0200 blanchet prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
Mon, 09 Aug 2010 10:13:18 +0200 blanchet reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF
Mon, 09 Aug 2010 09:57:38 +0200 blanchet fix embarrassing bug in elim rule handling, introduced during the port to FOF
Thu, 05 Aug 2010 12:40:12 +0200 blanchet fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
Fri, 30 Jul 2010 00:02:25 +0200 blanchet don't choke on synonyms when parsing SPASS's Flotter output + renamings;
Thu, 29 Jul 2010 23:11:35 +0200 blanchet fix bug in the newly introduced "bound concealing" code
Thu, 29 Jul 2010 22:43:46 +0200 blanchet use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
Thu, 29 Jul 2010 21:20:24 +0200 blanchet handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
Thu, 29 Jul 2010 18:45:41 +0200 blanchet speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
Thu, 29 Jul 2010 17:45:22 +0200 blanchet work around atomization failures
Thu, 29 Jul 2010 16:41:32 +0200 blanchet perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
Thu, 29 Jul 2010 16:11:02 +0200 blanchet fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
Thu, 29 Jul 2010 15:50:26 +0200 blanchet generate correct names for "$true" and "$false";
Thu, 29 Jul 2010 15:37:27 +0200 blanchet don't assume canonical rule format
Thu, 29 Jul 2010 14:53:55 +0200 blanchet avoid "clause" and "cnf" terminology where it no longer makes sense
Thu, 29 Jul 2010 14:42:09 +0200 blanchet "axiom_clauses" -> "axioms" (these are no longer clauses)
Thu, 29 Jul 2010 14:39:43 +0200 blanchet remove the "extra_clauses" business introduced in 19a5f1c8a844;
Wed, 28 Jul 2010 23:01:27 +0200 blanchet handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
Wed, 28 Jul 2010 18:54:18 +0200 blanchet minor refactoring
Wed, 28 Jul 2010 18:07:25 +0200 blanchet fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
Wed, 28 Jul 2010 17:38:40 +0200 blanchet revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
Wed, 28 Jul 2010 10:45:49 +0200 blanchet renaming
Wed, 28 Jul 2010 00:53:24 +0200 blanchet improve detection of installed SPASS
Tue, 27 Jul 2010 19:41:19 +0200 blanchet minor refactoring
Tue, 27 Jul 2010 18:33:10 +0200 blanchet more refactoring
Tue, 27 Jul 2010 17:56:01 +0200 blanchet rename "ATP_Manager" ML module to "Sledgehammer";
Tue, 27 Jul 2010 17:49:16 +0200 blanchet rename
less more (0) tip