| Mon, 12 Oct 2020 18:59:44 +0200 | Mathias Fleury | add reconstruction for the SMT solver veriT | file | diff | annotate |
| Thu, 02 Oct 2014 17:39:38 +0200 | blanchet | avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition | file | diff | annotate |
| Tue, 30 Sep 2014 12:47:15 +0200 | blanchet | repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices' | file | diff | annotate |
| Tue, 30 Sep 2014 11:06:26 +0200 | blanchet | keep rules with no premises in Isar proofs from veriT | file | diff | annotate |
| Mon, 29 Sep 2014 18:37:33 +0200 | blanchet | simplified and repaired veriT index handling code | file | diff | annotate |
| 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 | file | diff | annotate |
| Thu, 28 Aug 2014 00:40:38 +0200 | blanchet | renamed new SMT module from 'SMT2' to 'SMT' | file | diff | annotate | base |