src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2013-11-19 ago more refactoring to accommodate SMT proofs
2013-11-19 ago refactoring
2013-11-19 ago refactored
2013-11-14 ago implemented 'tptp_translate'
2013-10-17 ago generate a comment storing the goal nickname in "learn_prover"
2013-10-17 ago if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
2013-10-17 ago if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
2013-10-10 ago simplify fudge factor code
2013-10-09 ago cleanup SMT-related config options
2013-10-09 ago use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
2013-10-08 ago higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
2013-09-30 ago added experimental configuration options to tune use of builtin symbols in SMT
2013-09-30 ago minor tweak to error message
2013-09-23 ago added "spy" option to Sledgehammer
2013-09-20 ago merged "isar_try0" and "isar_minimize" options
2013-09-20 ago hardcoded obscure option
2013-09-20 ago hard-coded an obscure option
2013-09-20 ago use configuration mechanism for low-level tracing
2013-09-12 ago prefixed types and some functions with "atp_" for disambiguation
2013-09-11 ago killed dead code
2013-09-11 ago speed up often-called function
2013-09-10 ago don't be so verbose about SMT solver failures
2013-09-09 ago since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
2013-09-09 ago limit the number of instances of a single theorem
2013-09-09 ago use new monomorphizer in Sledgehammer
2013-08-22 ago tuning
2013-08-17 ago sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
2013-08-17 ago more explicit sendback propertries based on mode;
2013-08-13 ago added flag for jEdit/PIDE asynchronous mode
2013-07-29 ago added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
2013-07-18 ago explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-12 ago added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
2013-07-09 ago completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-07-09 ago moved code -> easier debugging
2013-05-28 ago redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-26 ago handle lambda-lifted problems in Isar construction code
2013-05-24 ago improved handling of free variables' types in Isar proofs
2013-05-16 ago correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
2013-05-16 ago tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-06 ago added preplay tracing
2013-03-28 ago new, simpler implementation of monomorphization;
2013-02-21 ago tuned misleading message
2013-02-21 ago generate Isar proof if Metis appears to be too slow
2013-02-20 ago don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary
2013-02-20 ago minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
2013-02-20 ago made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
2013-02-19 ago interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
2013-02-18 ago implement (more) accurate computation of parents
2013-02-14 ago renamed sledgehammer_shrink to sledgehammer_compress
2013-02-07 ago distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
2013-01-31 ago also have SMT solvers alternate fact filter
2013-01-31 ago use the right filter in each slice
2013-01-31 ago store fact filter along with ATP slice
2013-01-31 ago tuned data structure
2013-01-31 ago thread through fact triple component from which used facts come, for accurate index output
2013-01-31 ago thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
2013-01-31 ago eliminated needless speed optimization -- and simplified code quite a bit
2013-01-17 ago added E-Par support
2013-01-07 ago cleaner context threading