| Tue, 27 Mar 2012 14:46:34 +0200 | kuncar | note a code eqn in quotient_def | changeset | files |
| Tue, 27 Mar 2012 17:11:02 +0200 | boehmes | dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct | changeset | files |
| Tue, 27 Mar 2012 16:59:13 +0300 | blanchet | more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts) | changeset | files |
| Tue, 27 Mar 2012 16:59:13 +0300 | blanchet | fixed eta-extension of higher-order quantifiers in THF output | changeset | files |
| Tue, 27 Mar 2012 16:59:13 +0300 | blanchet | renamed "smt_fixed" to "smt_read_only_certificates" | changeset | files |
| Tue, 27 Mar 2012 16:59:13 +0300 | blanchet | tuning | changeset | files |