| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | properly unmangle names in path finder | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | only uncombine combinators in textual Isar proofs, not in Metis | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | properly locate helpers whose constants have several entries in the helper table | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | skip "hBOOL" in new Metis path finder | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | don't pass "~ " to 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 | gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | temporarily document "metisX" | changeset | files |