| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | don't translate new Skolemizer assumptions in new Metis | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | tuning | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | fixed detection of Skolem constants in type construction detection code | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis) | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | tuning | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | reveal Skolems in new Metis | changeset | files |