Mon, 14 Apr 2008 21:44:53 +0200 | wenzelm | avoid duplicate fact bindings; | file | diff | annotate |
Fri, 19 Oct 2007 23:21:08 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
Sun, 12 Aug 2007 18:53:03 +0200 | wenzelm | added type constraints to resolve syntax ambiguities; | file | diff | annotate |
Tue, 31 Jul 2007 14:45:36 +0200 | narboux | undo a change in last commit : give a single name to the inversion lemmas for the same inductive type | file | diff | annotate |
Mon, 30 Jul 2007 10:39:12 +0200 | urbanc | updated some of the definitions and proofs | file | diff | annotate |
Wed, 11 Jul 2007 11:36:06 +0200 | berghofe | Renamed inductive2 to inductive. | file | diff | annotate |