src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
2013-11-19 ago tuning
2013-10-17 ago generate a comment storing the goal nickname in "learn_prover"
2013-10-17 ago thread the goal through instead of relying on unreliable (possibly fake) state
2013-10-17 ago verbose minimization when learning from ATP proofs
2013-10-16 ago have MaSh minimize
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-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-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-02-20 ago minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
2013-02-20 ago auto-minimizer should respect "isar_proofs = true"
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 avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
2013-02-14 ago renamed sledgehammer_shrink to sledgehammer_compress
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-02 ago use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
2013-01-02 ago tuning
2012-12-15 ago thread no timeout properly
2012-11-06 ago renamed Sledgehammer option
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18 ago refactor code
2012-08-14 ago warn users about unused "using" facts
2012-08-14 ago be less aggressive at kicking out chained facts
2012-08-14 ago consider removing chained facts last, so that they're more likely to be kept
2012-07-20 ago learn from SMT proofs when they can be minimized by Metis
2012-07-20 ago name tuning
2012-07-20 ago fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 ago added "learn_from_atp" command to MaSh, for patient users
2012-07-20 ago learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-18 ago learn from minimized ATP proofs
2012-07-18 ago added option to control which fact filter is used
2012-07-18 ago renamed Sledgehammer options
2012-07-18 ago more code rationalization in relevance filter
2012-07-11 ago further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-06-06 ago avoid dumping definitions several times in LEO-II proofs
2012-04-18 ago get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
2012-02-04 ago made option available to users (mostly for experiments)
2012-02-01 ago proper statuses for "fact_from_ref"
2012-01-26 ago separate orthogonal components
2012-01-23 ago renamed two files to make room for a new file
2012-01-19 ago renamed "sound" option to "strict"
2011-12-01 ago added "minimize" option for more control over automatic minimization
2011-12-01 ago renamed "slicing" to "slice"
2011-11-18 ago be more silent when auto minimizing
2011-11-16 ago thread in additional options to minimizer
2011-11-16 ago make metis reconstruction handling more flexible
2011-11-16 ago parse lambda translation option in Metis
2011-11-06 ago cascading timeouts in minimizer, part 2
2011-11-06 ago tuning