src/HOL/Tools/SMT2/smt2_normalize.ML
2014-06-03 blanchet 2014-06-03 removed SMT weights -- their impact was very inconclusive anyway
2014-05-16 blanchet 2014-05-16 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-13 blanchet 2014-03-13 avoid name clash
2014-03-13 blanchet 2014-03-13 simplify index handling
2014-03-13 blanchet 2014-03-13 more robust indices
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 move lemmas to theory file, towards textual proof reconstruction
2014-03-13 blanchet 2014-03-13 tuning
2014-03-13 blanchet 2014-03-13 adapted to renamed ML files
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle