src/HOL/Tools/SMT/verit_isar.ML
Thu, 02 Oct 2014 17:39:38 +0200 blanchet avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition
Tue, 30 Sep 2014 12:47:15 +0200 blanchet repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
Tue, 30 Sep 2014 11:06:26 +0200 blanchet keep rules with no premises in Isar proofs from veriT
Mon, 29 Sep 2014 18:37:33 +0200 blanchet simplified and repaired veriT index handling code
Thu, 28 Aug 2014 00:40:38 +0200 blanchet keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
less more (0) tip