Thu, 27 Feb 2003 15:12:29 +0100 | ballarin | Change to meta simplifier: congruence rules may now have frees as head of term. | changeset | files |
Wed, 26 Feb 2003 14:26:18 +0100 | kleing | == -> = | changeset | files |
Wed, 26 Feb 2003 13:16:07 +0100 | paulson | zprime_def fixes by Jeremy Avigad | changeset | files |