Fri, 12 Mar 1999 22:02:51 +0100 | wenzelm | made weblint happy; | file | diff | annotate |
Wed, 14 Oct 1998 15:47:22 +0200 | nipkow | Description of new version. | file | diff | annotate |
Wed, 14 Oct 1998 15:26:31 +0200 | nipkow | New many-sorted version. | file | diff | annotate |
Thu, 02 May 1996 10:20:15 +0200 | nipkow | Added note on types. | file | diff | annotate |
Fri, 17 Nov 1995 09:04:10 +0100 | nipkow | New directory. | file | diff | annotate |