src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
2012-11-06 blanchet 2012-11-06 renamed Sledgehammer option
2012-10-18 blanchet 2012-10-18 renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18 blanchet 2012-10-18 refactor code
2012-08-14 blanchet 2012-08-14 warn users about unused "using" facts
2012-08-14 blanchet 2012-08-14 be less aggressive at kicking out chained facts
2012-08-14 blanchet 2012-08-14 consider removing chained facts last, so that they're more likely to be kept
2012-07-20 blanchet 2012-07-20 learn from SMT proofs when they can be minimized by Metis
2012-07-20 blanchet 2012-07-20 name tuning
2012-07-20 blanchet 2012-07-20 fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 blanchet 2012-07-20 added "learn_from_atp" command to MaSh, for patient users
2012-07-20 blanchet 2012-07-20 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-18 blanchet 2012-07-18 learn from minimized ATP proofs
2012-07-18 blanchet 2012-07-18 added option to control which fact filter is used
2012-07-18 blanchet 2012-07-18 renamed Sledgehammer options
2012-07-18 blanchet 2012-07-18 more code rationalization in relevance filter
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-06-06 blanchet 2012-06-06 avoid dumping definitions several times in LEO-II proofs
2012-04-18 blanchet 2012-04-18 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 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-02-01 blanchet 2012-02-01 proper statuses for "fact_from_ref"
2012-01-26 blanchet 2012-01-26 separate orthogonal components
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2012-01-19 blanchet 2012-01-19 renamed "sound" option to "strict"
2011-12-01 blanchet 2011-12-01 added "minimize" option for more control over automatic minimization
2011-12-01 blanchet 2011-12-01 renamed "slicing" to "slice"
2011-11-18 blanchet 2011-11-18 be more silent when auto minimizing
2011-11-16 blanchet 2011-11-16 thread in additional options to minimizer
2011-11-16 blanchet 2011-11-16 make metis reconstruction handling more flexible
2011-11-16 blanchet 2011-11-16 parse lambda translation option in Metis
2011-11-06 blanchet 2011-11-06 cascading timeouts in minimizer, part 2
2011-11-06 blanchet 2011-11-06 tuning
2011-11-06 blanchet 2011-11-06 use "Time.time" rather than milliseconds internally
2011-11-06 blanchet 2011-11-06 tune: no need for option
2011-11-06 blanchet 2011-11-06 cascading timeouts in minimizer
2011-11-06 blanchet 2011-11-06 shortcut binary minimization algorithm
2011-11-06 blanchet 2011-11-06 speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
2011-08-24 blanchet 2011-08-24 make sure that all facts are passed to ATP from minimizer
2011-07-01 blanchet 2011-07-01 made minimizer informative output accurate
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate
2011-06-27 blanchet 2011-06-27 clarify minimizer output
2011-06-27 blanchet 2011-06-27 added "sound" option to force Sledgehammer to be pedantically sound
2011-06-09 blanchet 2011-06-09 tuning
2011-06-08 blanchet 2011-06-08 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
2011-06-08 blanchet 2011-06-08 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-06 blanchet 2011-06-06 show what failed to play
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-30 blanchet 2011-05-30 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30 blanchet 2011-05-30 minimize automatically even if Metis failed, if the external prover was really fast
2011-05-30 blanchet 2011-05-30 automatically minimize with Metis when this can be done within a few seconds
2011-05-30 blanchet 2011-05-30 minimize with Metis if possible
2011-05-30 blanchet 2011-05-30 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-29 blanchet 2011-05-29 normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-27 blanchet 2011-05-27 show time taken for reconstruction
2011-05-27 blanchet 2011-05-27 handle non-auto try case of Sledgehammer better
2011-05-27 blanchet 2011-05-27 renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27 blanchet 2011-05-27 added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27 blanchet 2011-05-27 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-12 blanchet 2011-05-12 renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts