src/HOL/Sledgehammer.thy
Fri, 12 Jul 2013 14:18:06 +0200 smolkas minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
Thu, 11 Jul 2013 20:08:06 +0200 smolkas optimize isar-proofs by trying different proof methods
Tue, 09 Jul 2013 18:44:59 +0200 smolkas moved code -> easier debugging
Mon, 18 Feb 2013 12:16:27 +0100 smolkas split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
Mon, 18 Feb 2013 12:16:02 +0100 smolkas simplified byline, isar_qualifier
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
Thu, 17 Jan 2013 11:55:40 +0100 smolkas move preplaying to own structure
Wed, 28 Nov 2012 12:25:43 +0100 smolkas renamed sledgehammer_isar_reconstruct to sledgehammer_proof
Wed, 28 Nov 2012 12:22:17 +0100 smolkas put shrink in own structure
Wed, 28 Nov 2012 12:22:05 +0100 smolkas put annotate in own structure
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
less more (0) -60 tip