src/HOL/Tools/SMT/verit_isar.ML
2014-10-02 blanchet 2014-10-02 avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition
2014-09-30 blanchet 2014-09-30 repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
2014-09-30 blanchet 2014-09-30 keep rules with no premises in Isar proofs from veriT
2014-09-29 blanchet 2014-09-29 simplified and repaired veriT index handling code
2014-08-28 blanchet 2014-08-28 keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'