| Mon, 08 Aug 1994 16:45:08 +0200 | nipkow | Simplified some proofs. Added some type assumptions to the introduction rules. | file | diff | annotate |
| Fri, 29 Jul 1994 11:09:45 +0200 | lcp | Inductive defs need no longer mention SigmaI/E2 | file | diff | annotate |
| Thu, 21 Jul 1994 14:27:00 +0200 | nipkow | Initial revision | file | diff | annotate |