src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
2016-04-02 ago prefer infix operations;
2016-03-28 ago early warning when Sledgehammer finds a proof
2016-03-03 ago clarified modules;
2015-08-13 ago tuned signature, in accordance to sortBy in Scala;
2015-04-25 ago made CVC4 support work also without unsat cores
2014-11-20 ago other way of crashing (with CVC4)
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-09-30 ago tuned output in case of one-liner failure
2014-08-28 ago renamed new SMT module from 'SMT2' to 'SMT'
2014-06-12 ago reintroduced vital 'Thm.transfer'
2014-05-23 ago removed noise
2014-05-22 ago tuning
2014-05-16 ago correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-13 ago integrate SMT2 with Sledgehammer
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-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 merged 'reconstructors' and 'proof methods'
2014-01-31 ago tuning
2014-01-31 ago moved ML code around
2014-01-31 ago refactor large ML file