| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is | changeset | files |
| 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 |