| Wed, 13 Jun 2007 00:01:41 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Mon, 11 Dec 2006 16:06:14 +0100 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Mon, 11 Sep 2006 21:35:19 +0200 | wenzelm | induct method: renamed 'fixing' to 'arbitrary'; | file | diff | annotate |