src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
2014-06-02 ago basic setup for zipperposition prover
2014-05-16 ago silence methods even better
2014-05-15 ago new approach to silence proof methods, to avoid weird theory/context mismatches
2014-05-04 ago improved whitelist (cf. be1874de8344)
2014-04-19 ago more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
2014-04-08 ago more uniform ML/document antiquotations;
2014-03-31 ago support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
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