| 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 |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | added Metis examples to test the new type encodings | changeset | files |