src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
2016-04-02 ago prefer infix operations;
2016-02-01 ago preplaying of 'smt' and 'metis' more in sync with actual method
2015-10-02 ago further reduced dependency on legacy async thread manager
2015-05-28 ago took out Sledgehammer minimizer optimization that breaks things
2014-08-28 ago removed show stuttering
2014-08-28 ago made trace more informative when minimization is enabled
2014-08-28 ago tuned tracing output (indirectly)
2014-08-04 ago sort facts in minimizer as well
2014-08-01 ago tuning
2014-08-01 ago simplified minimization logic
2014-08-01 ago tuning
2014-07-30 ago tuned ML function name
2014-07-25 ago faster minimization by not adding facts that are already in the simpset
2014-05-22 ago tuning
2014-02-13 ago avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
2014-02-04 ago tuned slack
2014-02-04 ago tuning
2014-02-03 ago generate comments in Isar proofs
2014-02-03 ago keep all proof methods in data structure until the end, to enhance debugging output
2014-02-03 ago renamed ML file
2014-02-03 ago tuned data structure
2014-02-03 ago more flexible compression, choosing whichever proof method works
2014-02-03 ago tuning
2014-02-03 ago centralize more preplaying
2014-02-03 ago tuning
2014-02-03 ago centralize preplaying
2014-02-03 ago tuned
2014-02-02 ago more data structure rationalization
2014-02-02 ago tuning
2014-02-02 ago more data structure rationalization
2014-02-02 ago refactoring of data structure (step 2)
2014-02-02 ago refactor data structure (step 1)
2014-02-02 ago simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
2014-02-02 ago reset timing information after changes
2014-01-31 ago generalized preplaying infrastructure to store various results for various methods
2014-01-31 ago tuning
2014-01-31 ago tuned ML function names
2014-01-31 ago tuning
2014-01-31 ago renamed many Sledgehammer ML files to clarify structure