src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
2016-04-02 ago prefer infix operations;
2016-02-01 ago preplaying of 'smt' and 'metis' more in sync with actual method
2015-11-14 ago more standard ML, to make SML/NJ more happy;
2015-11-10 ago generalized so that is also works for veriT proofs
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-08 ago added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-08-04 ago rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-01 ago fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01 ago careful when compressing 'obtains'
2014-08-01 ago try to get rid of skolems first
2014-08-01 ago no need to 'obtain' variables not in formula
2014-07-31 ago cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-30 ago also try 'metis' with 'full_types'
2014-06-24 ago don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
2014-06-12 ago renamed Sledgehammer options
2014-06-02 ago avoid division by 0
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