| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | temporarily document "metisX" | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | use "metisX" as fallback, since it's much faster than "metisFT" | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | temporarily added "MetisX" as reconstructor and minimizer | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis) | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | show what failed to play | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | tuning | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | killed odd connectives | changeset | files |