src/HOL/Sledgehammer.thy
Tue, 16 Oct 2012 18:50:53 +0200 blanchet added proof minimization code from Steffen Smolka
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML files
Wed, 18 Jul 2012 08:44:03 +0200 blanchet rationalize relevance filter, slowing moving code from Iter to MaSh
Wed, 11 Jul 2012 21:43:19 +0200 blanchet moved most of MaSh exporter code to Sledgehammer
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Thu, 09 Dec 2010 08:46:04 +0100 blanchet compile
Wed, 08 Dec 2010 22:17:52 +0100 blanchet split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
Tue, 07 Dec 2010 09:58:56 +0100 blanchet load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
Tue, 26 Oct 2010 13:16:43 +0200 blanchet integrated "smt" proof method with Sledgehammer
Tue, 26 Oct 2010 12:17:19 +0200 blanchet reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies
Fri, 22 Oct 2010 13:54:51 +0200 blanchet renamed files
Tue, 05 Oct 2010 11:10:37 +0200 blanchet factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
Mon, 04 Oct 2010 22:51:53 +0200 blanchet tuning
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain
Mon, 04 Oct 2010 21:50:32 +0200 blanchet remove Meson from Sledgehammer
Thu, 30 Sep 2010 18:59:37 +0200 blanchet encode number of skolem assumptions in them, for more efficient retrieval later
Wed, 29 Sep 2010 23:30:10 +0200 blanchet finished renaming file and module
Wed, 29 Sep 2010 23:26:39 +0200 blanchet rename file
Mon, 27 Sep 2010 10:44:08 +0200 blanchet rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
Thu, 16 Sep 2010 16:24:23 +0200 blanchet added new "Metis_Reconstruct" module, temporarily empty
Thu, 16 Sep 2010 16:12:02 +0200 blanchet rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing;
Tue, 14 Sep 2010 09:12:28 +0200 blanchet rename internal Sledgehammer constant
Sat, 11 Sep 2010 10:25:27 +0200 blanchet setup Auto Sledgehammer
Thu, 02 Sep 2010 11:29:02 +0200 blanchet use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
Wed, 01 Sep 2010 00:03:15 +0200 blanchet finish moving file
Tue, 31 Aug 2010 23:50:59 +0200 blanchet finished renaming
Thu, 19 Aug 2010 18:16:47 +0200 blanchet encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
Wed, 28 Jul 2010 19:04:59 +0200 blanchet consequence of directory renaming
Tue, 27 Jul 2010 19:41:19 +0200 blanchet minor refactoring
Tue, 27 Jul 2010 19:17:15 +0200 blanchet standardize "Author" tags
Tue, 27 Jul 2010 18:45:55 +0200 blanchet reorder ML files in theory
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:43:11 +0200 blanchet complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
Mon, 28 Jun 2010 18:47:07 +0200 blanchet no setup is necessary anymore
Fri, 25 Jun 2010 18:05:36 +0200 blanchet factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
Fri, 25 Jun 2010 17:13:38 +0200 blanchet reorder ML files
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
Fri, 25 Jun 2010 15:30:38 +0200 blanchet more moving around of ML files in "Sledgehammer.thy"
Fri, 25 Jun 2010 15:18:58 +0200 blanchet move "MESON" up;
Thu, 24 Jun 2010 17:57:36 +0200 blanchet never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
Wed, 23 Jun 2010 09:40:06 +0200 blanchet killed legacy "neg_clausify" and "clausify"
Tue, 22 Jun 2010 23:54:02 +0200 blanchet factor out TPTP format output into file of its own, to facilitate further changes
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"
Fri, 11 Jun 2010 17:10:23 +0200 blanchet proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
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)
Sun, 25 Apr 2010 14:40:36 +0200 blanchet move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
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
Fri, 23 Apr 2010 18:06:41 +0200 blanchet renamed module "ATP_Wrapper" to "ATP_Systems"
Fri, 23 Apr 2010 17:38:25 +0200 blanchet move the minimizer to the Sledgehammer directory
Mon, 29 Mar 2010 19:49:57 +0200 blanchet added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
less more (0) -60 tip