src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-15 blanchet 2010-11-15 turn on Sledgehammer verbosity so we can track down crashes
2010-11-13 wenzelm 2010-11-13 total Symbol.source;
2010-11-07 blanchet 2010-11-07 always use a hard timeout in Mirabelle
2010-11-07 blanchet 2010-11-07 use "smt" (rather than "metis") to reconstruct SMT proofs
2010-11-05 blanchet 2010-11-05 make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-04 blanchet 2010-11-04 remove " s" suffix since seconds are now implicit
2010-11-04 blanchet 2010-11-04 use the SMT integration's official list of built-ins
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26 blanchet 2010-10-26 remove needless context argument; prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"
2010-10-26 blanchet 2010-10-26 proper error handling for SMT solvers in Sledgehammer
2010-10-22 blanchet 2010-10-22 tuning
2010-10-22 blanchet 2010-10-22 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
2010-10-22 blanchet 2010-10-22 replaced references with proper record that's threaded through
2010-10-22 blanchet 2010-10-22 fixed signature of "is_smt_solver_installed"; renaming
2010-10-22 blanchet 2010-10-22 remove more needless code ("run_smt_solvers"); tuning
2010-10-22 blanchet 2010-10-22 bring ATPs and SMT solvers more in line with each other
2010-10-22 blanchet 2010-10-22 make Sledgehammer minimizer fully work with SMT
2010-10-22 blanchet 2010-10-22 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
2010-10-21 blanchet 2010-10-21 first step in adding support for an SMT backend to Sledgehammer
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-14 blanchet 2010-09-14 tuning
2010-09-14 blanchet 2010-09-14 handle relevance filter corner cases more gracefully; e.g. the minimizer selects 15 facts but "max_relevant = 14"
2010-09-14 blanchet 2010-09-14 added a timeout around "try" call in Mirabelle
2010-09-13 blanchet 2010-09-13 indicate triviality in the list of proved things
2010-09-13 blanchet 2010-09-13 indicate which goals are trivial
2010-09-13 blanchet 2010-09-13 keep track of trivial vs. nontrivial calls using "try" for 30 seconds
2010-09-11 blanchet 2010-09-11 make Mirabelle happy
2010-09-01 blanchet 2010-09-01 minor refactoring
2010-09-01 blanchet 2010-09-01 translate the axioms to FOF once and for all ATPs
2010-09-01 blanchet 2010-09-01 run relevance filter in a thread, to avoid blocking
2010-09-01 blanchet 2010-09-01 share the relevance filter among the provers
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-27 blanchet 2010-08-27 drop chained facts
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-24 blanchet 2010-08-24 make Mirabelle happy
2010-08-18 blanchet 2010-08-18 get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-07-29 blanchet 2010-07-29 fix Mirabelle timeout
2010-07-29 blanchet 2010-07-29 make Mirabelle happy
2010-07-29 blanchet 2010-07-29 "axiom_clauses" -> "axioms" (these are no longer clauses)
2010-07-27 blanchet 2010-07-27 compile
2010-07-27 blanchet 2010-07-27 implemented "sublinear" minimization algorithm
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-06-29 blanchet 2010-06-29 compile
2010-06-29 blanchet 2010-06-29 compile
2010-06-28 blanchet 2010-06-28 compile
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-22 blanchet 2010-06-22 turn on "natural form" filtering in the Mirabelle tests, to see how it performs
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-04-28 blanchet 2010-04-28 make Mirabelle happy
2010-04-26 blanchet 2010-04-26 compile
2010-04-23 blanchet 2010-04-23 move some sledgehammer stuff out of "atp_manager.ML"
2010-04-23 blanchet 2010-04-23 compile
2010-04-19 blanchet 2010-04-19 make Sledgehammer's minimizer also minimize Isar proofs