| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | reveal Skolems in new Metis | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | slacker version of "fastype_of", in case a function has dummy type | changeset | files |
| 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 |