| Fri, 22 Oct 2010 13:48:21 +0200 | blanchet | remove more needless code ("run_smt_solvers"); | changeset | files |
| Fri, 22 Oct 2010 12:15:31 +0200 | blanchet | got rid of duplicate functionality ("run_smt_solver_somehow"); | changeset | files |
| Fri, 22 Oct 2010 11:58:33 +0200 | blanchet | bring ATPs and SMT solvers more in line with each other | changeset | files |
| Fri, 22 Oct 2010 11:11:34 +0200 | blanchet | make Sledgehammer minimizer fully work with SMT | changeset | files |
| Fri, 22 Oct 2010 09:50:18 +0200 | blanchet | generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well | changeset | files |
| Thu, 21 Oct 2010 16:25:40 +0200 | blanchet | first step in adding support for an SMT backend to Sledgehammer | changeset | files |
| Thu, 21 Oct 2010 14:55:09 +0200 | blanchet | use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..." | changeset | files |