src/HOL/Sledgehammer.thy
Thu, 28 Aug 2014 16:58:27 +0200 blanchet moved skolem method
Thu, 28 Aug 2014 16:58:27 +0200 blanchet added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Mon, 16 Jun 2014 19:41:42 +0200 blanchet fixed parsing of one-argument 'file()' in TSTP files
Mon, 16 Jun 2014 19:41:01 +0200 blanchet use right delimiters for Waldmeister proofs
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code
Mon, 16 Jun 2014 19:40:04 +0200 blanchet moved code around
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuned dependencies
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies
Wed, 11 Jun 2014 15:29:23 +0200 blanchet moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer
Fri, 14 Mar 2014 11:15:46 +0100 blanchet undo rewrite rules (e.g. for 'fun_app') in Isar
Fri, 14 Mar 2014 11:05:44 +0100 blanchet more simplification of trivial steps
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file
Mon, 03 Feb 2014 10:14:18 +0100 blanchet got rid of 'try0' step that is now redundant
Fri, 31 Jan 2014 16:07:20 +0100 blanchet moved ML code around
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name
Fri, 20 Dec 2013 20:36:38 +0100 blanchet reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
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"
less more (0) -60 tip