Sat, 10 Oct 2015 20:54:44 +0200 | wenzelm | more symbols; | file | diff | annotate |
Sat, 10 Oct 2015 20:51:39 +0200 | wenzelm | more symbols; | file | diff | annotate |
Sat, 13 Mar 2010 16:44:12 +0100 | wenzelm | removed old CVS Ids; | file | diff | annotate |
Sun, 21 Feb 2010 20:54:40 +0100 | wenzelm | simplified syntax -- to make it work for authentic syntax; | file | diff | annotate |
Mon, 08 Feb 2010 21:28:27 +0100 | wenzelm | modernized some syntax translations; | file | diff | annotate |
Wed, 09 May 2007 19:37:20 +0200 | wenzelm | tuned syntax; | file | diff | annotate |
Tue, 21 Nov 2006 00:00:39 +0100 | wenzelm | converted legacy ML scripts; | file | diff | annotate |
Mon, 20 Nov 2006 23:47:10 +0100 | wenzelm | converted legacy ML scripts; | file | diff | annotate |