| Thu, 22 May 2008 16:34:41 +0200 | urbanc | made the naming of the induction principles consistent: weak_induct is | file | diff | annotate |
| Tue, 08 Jan 2008 23:11:08 +0100 | urbanc | tuned proofs | file | diff | annotate |
| Sun, 12 Aug 2007 18:53:03 +0200 | wenzelm | added type constraints to resolve syntax ambiguities; | file | diff | annotate |
| Wed, 11 Jul 2007 11:36:06 +0200 | berghofe | Renamed inductive2 to inductive. | file | diff | annotate |
| Thu, 21 Jun 2007 22:10:16 +0200 | wenzelm | tuned proofs -- avoid implicit prems; | file | diff | annotate |
| Mon, 11 Jun 2007 11:06:04 +0200 | chaieb | tuned Proof | file | diff | annotate |
| Mon, 04 Jun 2007 13:22:22 +0200 | urbanc | added a few comments to the proofs | file | diff | annotate |
| Thu, 31 May 2007 09:48:20 +0200 | urbanc | a theory using locally nameless terms and strong induction principles | file | diff | annotate |