| Fri, 02 May 2008 18:42:17 +0200 | urbanc | added mising lemma | file | diff | annotate |
| Tue, 08 Jan 2008 23:11:08 +0100 | urbanc | tuned proofs | file | diff | annotate |
| Fri, 04 Jan 2008 09:34:11 +0100 | urbanc | adapted to new inversion rules | file | diff | annotate |
| Mon, 08 Oct 2007 07:38:13 +0200 | urbanc | Isar-fied many proofs | file | diff | annotate |
| Tue, 24 Jul 2007 20:34:11 +0200 | urbanc | cleaned up the proofs a bit | file | diff | annotate |
| Wed, 11 Jul 2007 11:36:06 +0200 | berghofe | Renamed inductive2 to inductive. | file | diff | annotate |
| Thu, 14 Jun 2007 23:04:36 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |