| Sat, 18 Dec 2010 12:46:58 +0100 | blanchet | factored out running a prover with (optionally) an implicit minimizer phrase | changeset | files |
| Fri, 17 Dec 2010 23:18:39 +0100 | wenzelm | merged; | changeset | files |
| Fri, 17 Dec 2010 23:09:53 +0100 | blanchet | remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run) | changeset | files |
| Fri, 17 Dec 2010 22:15:08 +0100 | blanchet | more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle | changeset | files |
| Fri, 17 Dec 2010 21:47:13 +0100 | blanchet | convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented | changeset | files |
| Fri, 17 Dec 2010 21:32:06 +0100 | blanchet | merged | changeset | files |
| Fri, 17 Dec 2010 21:31:19 +0100 | blanchet | put the SMT weights back where they belong, so that they're also used by Mirabelle | changeset | files |