Thu, 03 Jan 2013 17:28:55 +0100 | blanchet | use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments) | changeset | files |
Thu, 03 Jan 2013 17:10:12 +0100 | blanchet | rename variable in binder, not just in body | changeset | files |