| Wed, 30 Nov 2005 15:27:30 +0100 | urbanc | added one clause for substitution in the lambda-case and | changeset | files |
| Wed, 30 Nov 2005 15:24:32 +0100 | wenzelm | added rename_params_rule: recover orginal fresh names in subgoals/cases; | changeset | files |
| Wed, 30 Nov 2005 15:03:15 +0100 | urbanc | changed induction principle and everything to conform with the | changeset | files |
| Wed, 30 Nov 2005 14:27:50 +0100 | wenzelm | fresh: frees instead of terms, rename corresponding params in rule; | changeset | files |
| Wed, 30 Nov 2005 14:27:09 +0100 | urbanc | adapted to the new nominal_induction | changeset | files |
| Wed, 30 Nov 2005 12:28:47 +0100 | urbanc | changed \<sim> of permutation equality to \<triangleq> | changeset | files |