Fri, 05 Oct 2007 23:04:14 +0200 | wenzelm | tuned proofs (via polymorphic taking''); | file | diff | annotate |
Fri, 05 Oct 2007 22:00:13 +0200 | wenzelm | coinduct: instantiation refers to suffix of main prop (major premise or conclusion); | file | diff | annotate |
Wed, 11 Jul 2007 11:28:13 +0200 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |