| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | don't stumble on Skolem names | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | conceal old Skolems in new Metis | changeset | files |
| 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 |