src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
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