src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
2016-04-02 ago prefer infix operations;
2016-03-05 ago tuned signature -- clarified modules;
2016-02-01 ago preplaying of 'smt' and 'metis' more in sync with actual method
2015-09-25 ago moved remaining display.ML to more_thm.ML;
2015-06-22 ago keep 'Pure.all' in goals when preplaying
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-09-24 ago tuning
2014-08-28 ago made trace more informative when minimization is enabled
2014-08-04 ago slightly earlier exit from preplaying
2014-08-01 ago rationalized preplaying by eliminating (now superfluous) laziness
2014-07-31 ago cascading timeout in parallel evaluation, to rapidly find optimum
2014-05-22 ago tuning
2014-03-13 ago simplified preplaying information
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 more generous Isar proof compression -- try to remove failing steps
2014-02-04 ago tweaked handling of 'hopeless' methods
2014-02-04 ago tuning
2014-02-03 ago don't lose additional outcomes
2014-02-03 ago properly overwrite replay data from one compression iteration to another
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 proper fresh name generation
2014-02-03 ago renamed ML file
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-02-03 ago added 'smt' as a proof method
2014-02-03 ago tuned data structure
2014-02-03 ago tuned data structure
2014-02-03 ago more flexible compression, choosing whichever proof method works
2014-02-03 ago less aggressive evaluation
2014-02-03 ago tuning
2014-02-03 ago more thorough, hybrid compression
2014-02-03 ago tuning
2014-02-03 ago centralize more preplaying
2014-02-03 ago centralize preplaying
2014-02-02 ago more data structure rationalization
2014-02-02 ago more data structure rationalization
2014-02-02 ago rationalized threading of 'metis' arguments
2014-02-02 ago refactored data structure (step 3)
2014-02-02 ago refactoring of data structure (step 2)
2014-02-02 ago unform treatment of preplay_timeout = 0 and > 0
2014-02-02 ago refactor data structure (step 1)
2014-02-02 ago tuned code
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 added 'algebra' to the mix
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