src/HOL/Sledgehammer.thy
2014-09-29 blanchet 2014-09-29 made 'moura' tactic more powerful
2014-08-28 blanchet 2014-08-28 moved skolem method
2014-08-28 blanchet 2014-08-28 added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-06-16 blanchet 2014-06-16 fixed parsing of one-argument 'file()' in TSTP files
2014-06-16 blanchet 2014-06-16 use right delimiters for Waldmeister proofs
2014-06-16 blanchet 2014-06-16 simplified code
2014-06-16 blanchet 2014-06-16 moved code around
2014-06-12 blanchet 2014-06-12 tuned dependencies
2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-06-11 blanchet 2014-06-11 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-11 blanchet 2014-06-11 removed old SMT module from Sledgehammer
2014-03-14 blanchet 2014-03-14 undo rewrite rules (e.g. for 'fun_app') in Isar
2014-03-14 blanchet 2014-03-14 more simplification of trivial steps
2014-03-13 blanchet 2014-03-13 integrate SMT2 with Sledgehammer
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-02-03 blanchet 2014-02-03 renamed ML file
2014-02-03 blanchet 2014-02-03 got rid of 'try0' step that is now redundant
2014-01-31 blanchet 2014-01-31 moved ML code around
2014-01-31 blanchet 2014-01-31 refactor large ML file
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure
2014-01-31 blanchet 2014-01-31 renamed ML file
2014-01-31 blanchet 2014-01-31 tuned ML file name
2013-12-20 blanchet 2013-12-20 reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-12 smolkas 2013-07-12 minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps
2013-07-11 smolkas 2013-07-11 optimize isar-proofs by trying different proof methods
2013-07-09 smolkas 2013-07-09 moved code -> easier debugging
2013-02-18 smolkas 2013-02-18 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
2013-02-18 smolkas 2013-02-18 simplified byline, isar_qualifier
2013-02-14 smolkas 2013-02-14 renamed sledgehammer_shrink to sledgehammer_compress
2013-01-17 smolkas 2013-01-17 move preplaying to own structure
2012-11-28 smolkas 2012-11-28 renamed sledgehammer_isar_reconstruct to sledgehammer_proof
2012-11-28 smolkas 2012-11-28 put shrink in own structure
2012-11-28 smolkas 2012-11-28 put annotate in own structure
2012-10-16 blanchet 2012-10-16 added proof minimization code from Steffen Smolka
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-20 blanchet 2012-07-20 renamed ML files
2012-07-18 blanchet 2012-07-18 rationalize relevance filter, slowing moving code from Iter to MaSh
2012-07-11 blanchet 2012-07-11 moved most of MaSh exporter code to Sledgehammer
2012-07-11 blanchet 2012-07-11 further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2010-12-09 blanchet 2010-12-09 compile
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-10-26 blanchet 2010-10-26 integrated "smt" proof method with Sledgehammer
2010-10-26 blanchet 2010-10-26 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
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-22 blanchet 2010-10-22 renamed files
2010-10-05 blanchet 2010-10-05 factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
2010-10-04 blanchet 2010-10-04 tuning
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-10-04 blanchet 2010-10-04 remove Meson from Sledgehammer
2010-09-30 blanchet 2010-09-30 encode number of skolem assumptions in them, for more efficient retrieval later
2010-09-29 blanchet 2010-09-29 finished renaming file and module
2010-09-29 blanchet 2010-09-29 rename file
2010-09-27 blanchet 2010-09-27 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-16 blanchet 2010-09-16 added new "Metis_Reconstruct" module, temporarily empty