Fri, 11 Mar 2022 09:22:13 +0100 |
desharna |
used more descriptive assert names in SMT-Lib output
|
file |
diff |
annotate
|
Tue, 13 Oct 2020 16:45:38 +0200 |
Mathias Fleury |
reconstruction of veriT proofs in NEWS
|
file |
diff |
annotate
|
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
|