Thu, 03 Jan 2013 17:10:12 +0100 | blanchet | rename variable in binder, not just in body | changeset | files |
Thu, 03 Jan 2013 15:13:11 +0100 | blanchet | swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases) | changeset | files |
Thu, 03 Jan 2013 14:41:05 +0100 | blanchet | tuned comment | changeset | files |