| Wed, 11 Jan 2006 18:39:19 +0100 | urbanc | cahges to use the new induction-principle (now proved in | changeset | files |
| Wed, 11 Jan 2006 18:38:32 +0100 | urbanc | changes to make use of the new induction principle proved by | changeset | files |
| Wed, 11 Jan 2006 18:21:23 +0100 | berghofe | Implemented proof of (strong) induction rule. | changeset | files |
| Wed, 11 Jan 2006 18:20:59 +0100 | berghofe | Added theorem at_finite_select. | changeset | files |
| Wed, 11 Jan 2006 17:12:30 +0100 | urbanc | added lemmas perm_empty, perm_insert to do with | changeset | files |
| Wed, 11 Jan 2006 17:10:11 +0100 | urbanc | merged the silly lemmas into the eqvt proof of subtype | changeset | files |
| Wed, 11 Jan 2006 17:07:57 +0100 | urbanc | tuned proofs | changeset | files |