src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
2014-06-02 ago basic setup for zipperposition prover
2014-05-22 ago properly reconstruct helpers in Z3 proofs
2014-05-22 ago tuning
2014-05-21 ago avoid markup-generating @{make_string}
2014-05-16 ago correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 ago use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-03-14 ago delayed construction of command (and of noncommercial check) + tuning
2014-03-13 ago simplified preplaying information
2014-03-13 ago honor the fact that the new Z3 can generate Isar proofs
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-13 ago repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
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-06 ago try right bunch of methods
2014-02-04 ago split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
2014-02-03 ago properly overwrite replay data from one compression iteration to another
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 renamed ML file
2014-02-03 ago tuning
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-01-31 ago tuning
2014-01-31 ago moved ML code around
2014-01-31 ago compile
2014-01-31 ago guarded against exception
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