/Admin/
drwxr-xr-x [up]
drwxr-xr-x Benchmarks HOL-datatype
drwxr-xr-x page
-rw-r--r-- 1999-08-26 11:33 +0200 590 BUGS
-rw-r--r-- 1999-08-26 11:33 +0200 378 MIRRORS
-rw-r--r-- 1999-08-26 11:33 +0200 137 README
-rwxr-xr-x 1999-08-26 11:33 +0200 2544 fixencoding
-rw-r--r-- 1999-08-26 11:33 +0200 2396 index.html
-rwxr-xr-x 1999-08-26 11:33 +0200 4402 makedist
-rwxr-xr-x 1999-08-26 11:33 +0200 6058 makerpm
-rwxr-xr-x 1999-08-26 11:33 +0200 203 psbooklet