2014-06-12 ago reintroduced vital 'Thm.transfer'
2014-06-03 ago removed SMT weights -- their impact was very inconclusive anyway
2014-06-02 ago refactored Z3 to Isar proof construction code
2014-06-02 ago simplified counterexample handling
2014-05-23 ago removed noise
2014-05-22 ago properly reconstruct helpers in Z3 proofs
2014-05-22 ago tuning
2014-05-16 ago correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 ago removed needless transfer
2014-05-16 ago use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-05-16 ago honor original format of conjecture or hypotheses in Z3-to-Isar proofs
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-14 ago delayed construction of command (and of noncommercial check) + tuning
2014-03-14 ago undo rewrite rules (e.g. for 'fun_app') in Isar
2014-03-13 ago correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
2014-03-13 ago thread through step IDs from Z3 to Sledgehammer
2014-03-13 ago let exception pass through in debug mode
2014-03-13 ago adapted to renamed ML files
2014-03-13 ago have Sledgehammer generate Isar proofs from Z3 proofs
2014-03-13 ago tuned ML interface
2014-03-13 ago integrate SMT2 with Sledgehammer