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
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
2010-09-14 blanchet 2010-09-14 rename internal Sledgehammer constant
2010-09-11 blanchet 2010-09-11 setup Auto Sledgehammer
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-09-01 blanchet 2010-09-01 finish moving file
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-19 blanchet 2010-08-19 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
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-07-28 blanchet 2010-07-28 consequence of directory renaming
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 standardize "Author" tags
2010-07-27 blanchet 2010-07-27 reorder ML files in theory
2010-07-27 blanchet 2010-07-27 more refactoring
2010-07-27 blanchet 2010-07-27 rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-06-28 blanchet 2010-06-28 no setup is necessary anymore
2010-06-25 blanchet 2010-06-25 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
2010-06-25 blanchet 2010-06-25 reorder ML files
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-25 blanchet 2010-06-25 more moving around of ML files in "Sledgehammer.thy"
2010-06-25 blanchet 2010-06-25 move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti
2010-06-24 blanchet 2010-06-24 never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
2010-06-23 blanchet 2010-06-23 killed legacy "neg_clausify" and "clausify"
2010-06-22 blanchet 2010-06-22 factor out TPTP format output into file of its own, to facilitate further changes
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-04-30 blanchet 2010-04-30 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
2010-04-25 blanchet 2010-04-25 move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
2010-04-23 blanchet 2010-04-23 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23 blanchet 2010-04-23 renamed module "ATP_Wrapper" to "ATP_Systems"
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory
2010-03-29 blanchet 2010-03-29 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used