src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
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