| Wed, 28 Apr 2010 16:05:38 +0200 | blanchet | add an Isar proof found with Sledgehammer that involves a Skolem constant (internally) | changeset | files |
| Wed, 28 Apr 2010 16:03:49 +0200 | blanchet | reintroduced short names for HOL->FOL constants; other parts of the code rely on these | changeset | files |
| Wed, 28 Apr 2010 15:53:17 +0200 | blanchet | save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code | changeset | files |
| Wed, 28 Apr 2010 15:34:55 +0200 | blanchet | unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction) | changeset | files |