Fri, 21 Nov 2014 13:18:56 +0100 | Andreas Lochbihler | add lemma following a proof suggestion by Joachim Breitner | changeset | files |
Fri, 21 Nov 2014 12:24:59 +0100 | Andreas Lochbihler | add lemma | changeset | files |
Fri, 21 Nov 2014 12:11:44 +0100 | Andreas Lochbihler | register pmf as BNF | changeset | files |
Thu, 20 Nov 2014 17:29:18 +0100 | blanchet | added CVC4 option that helps on JD | changeset | files |
Thu, 20 Nov 2014 17:29:18 +0100 | blanchet | always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says) | changeset | files |
Thu, 20 Nov 2014 17:29:18 +0100 | blanchet | work around bug in CVC4, with boolean arguments to (co)datatypes | changeset | files |