src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
2014-03-13 ago integrate SMT2 with Sledgehammer
2014-02-14 ago restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
2014-02-13 ago do the right thing with provers that exist only remotely (e.g. e_sine)
2014-02-03 ago renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 ago added 'smt' option to control generation of 'by smt' proofs
2014-02-03 ago tuning
2014-02-03 ago reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
2014-01-31 ago refactor large ML file
2014-01-31 ago renamed many Sledgehammer ML files to clarify structure
2014-01-31 ago renamed ML file
2014-01-31 ago tuned ML file name