| Fri, 28 May 1999 13:30:59 +0200 | wenzelm | tuned formal comments; | file | diff | annotate |
| Thu, 27 May 1999 20:49:10 +0200 | wenzelm | changed {| |} verbatim syntax to {* *}; | file | diff | annotate |
| Tue, 27 Apr 1999 10:46:37 +0200 | wenzelm | tuned; | file | diff | annotate |