Thu, 29 Jul 2010 22:13:15 +0200 | blanchet | fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis) | changeset | files |
Thu, 29 Jul 2010 21:20:24 +0200 | blanchet | handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs | changeset | files |
Thu, 29 Jul 2010 20:15:50 +0200 | blanchet | revert exception throwing in FOL_SOLVE, since they're not caught anyway | changeset | files |
Thu, 29 Jul 2010 20:02:02 +0200 | blanchet | avoid "ATP Error: Error: blah" style messages | changeset | files |
Thu, 29 Jul 2010 19:58:43 +0200 | blanchet | avoid "_def_raw" theorems | changeset | files |
Thu, 29 Jul 2010 19:26:42 +0200 | blanchet | better error and minimizer output | changeset | files |