src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
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-05 ago more exception cleanup + more liberal compressions of steps that timed out
2014-02-05 ago tuned code to avoid noncanonical (and risky) exception handling
2014-02-05 ago got rid of indices
2014-02-05 ago corrected wrong 'meth :: _' pattern maching + tuned code
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 tuned code
2014-02-04 ago split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
2014-02-04 ago tuning
2014-02-04 ago more liberal step merging
2014-02-03 ago don't lose additional outcomes
2014-02-03 ago tuning
2014-02-03 ago generate comments in Isar proofs
2014-02-03 ago allow merging of steps with subproofs
2014-02-03 ago renamed ML file
2014-02-03 ago when merging, don't try methods that failed or timed out for either of the steps for the combined step
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 better time slack, to account for ultra-quick proof methods
2014-02-03 ago crucial fix: use right version of the step
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-03 ago tuned
2014-02-02 ago more data structure rationalization
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 tuned factor
2014-02-02 ago take intersection rather than union of methods when merging steps -- more efficient and natural
2014-02-02 ago merge proof methods
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