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 |