src/HOL/Tools/SMT2/smt2_solver.ML
2014-05-16 blanchet 2014-05-16 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
2014-03-14 blanchet 2014-03-14 delayed construction of command (and of noncommercial check) + tuning
2014-03-14 blanchet 2014-03-14 tuning
2014-03-14 blanchet 2014-03-14 undo rewrite rules (e.g. for 'fun_app') in Isar
2014-03-14 blanchet 2014-03-14 tuning
2014-03-13 blanchet 2014-03-13 updated SMT2 examples and certificates
2014-03-13 blanchet 2014-03-13 simplify index handling
2014-03-13 blanchet 2014-03-13 correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
2014-03-13 blanchet 2014-03-13 thread through step IDs from Z3 to Sledgehammer
2014-03-13 blanchet 2014-03-13 avoid names that may clash with Z3's output (e.g. '')
2014-03-13 blanchet 2014-03-13 let exception pass through in debug mode
2014-03-13 blanchet 2014-03-13 adapted to renamed ML files
2014-03-13 blanchet 2014-03-13 slacker error code policy for Z3
2014-03-13 blanchet 2014-03-13 repaired 'if' logic
2014-03-13 blanchet 2014-03-13 have Sledgehammer generate Isar proofs from Z3 proofs
2014-03-13 blanchet 2014-03-13 tuned ML interface
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle