src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2014-03-14 ago undo rewrite rules (e.g. for 'fun_app') in Isar
2014-03-14 ago debugging stuff
2014-03-14 ago more simplification of trivial steps
2014-03-14 ago tuning
2014-03-13 ago tuning
2014-03-13 ago simplified preplaying information
2014-03-13 ago integrate SMT2 with Sledgehammer
2014-03-06 ago tuned signature;
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 do a second phase of proof compression after minimization
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-03 ago rationalized lists of methods
2014-02-03 ago extended method list
2014-02-03 ago generate comments in Isar proofs
2014-02-03 ago renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 ago tuned behavior of 'smt' option
2014-02-03 ago proper fresh name generation
2014-02-03 ago added 'smt' option to control generation of 'by smt' proofs
2014-02-03 ago renamed ML file
2014-02-03 ago tuning
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-02-03 ago tuning
2014-02-03 ago tuned data structure
2014-02-03 ago tuned data structure
2014-02-03 ago less aggressive evaluation
2014-02-03 ago added a new version of 'metis' to the mix
2014-02-03 ago implemented new 'try0_isar' semantics
2014-02-03 ago got rid of 'try0' step that is now redundant
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 rationalized threading of 'metis' arguments
2014-02-02 ago refactored data structure (step 3)
2014-02-02 ago unform treatment of preplay_timeout = 0 and > 0
2014-02-02 ago use Skolem proof methods appropriately
2014-02-02 ago simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
2014-01-31 ago generalized preplaying infrastructure to store various results for various methods
2014-01-31 ago added a 'trace' option
2014-01-31 ago moved code around
2014-01-31 ago added 'algebra' to the mix
2014-01-31 ago more informative trace
2014-01-31 ago better tracing + syntactically correct 'metis' calls
2014-01-31 ago tuned ML function names
2014-01-31 ago tuning
2014-01-31 ago moved ML code around
2014-01-31 ago renamed many Sledgehammer ML files to clarify structure
2014-01-30 ago renamed Sledgehammer options for symmetry between positive and negative versions
2013-12-19 ago made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-11-21 ago fixed spying so that the envirnoment variables are queried at run-time not at build-time
2013-11-19 ago tuning
2013-10-17 ago added comment
2013-10-15 ago use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
2013-10-04 ago run fewer provers in "try" mode
2013-10-04 ago count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)
2013-09-23 ago added "spy" option to Sledgehammer
2013-09-20 ago merged "isar_try0" and "isar_minimize" options