/lib/Tools/
drwxr-xr-x [up]
-rwxr-xr-x 2000-11-21 19:02 +0100 863 browser
-rwxr-xr-x 2000-11-21 19:02 +0100 883 doc
-rwxr-xr-x 2000-11-21 19:02 +0100 2163 document
-rwxr-xr-x 2000-11-21 19:02 +0100 856 expandshort
-rwxr-xr-x 2000-11-21 19:02 +0100 653 findlogics
-rwxr-xr-x 2000-11-21 19:02 +0100 695 fixclasimp
-rwxr-xr-x 2000-11-21 19:02 +0100 730 fixdatatype
-rwxr-xr-x 2000-11-21 19:02 +0100 757 fixdots
-rwxr-xr-x 2000-11-21 19:02 +0100 706 fixgoal
-rwxr-xr-x 2000-11-21 19:02 +0100 705 fixseq
-rwxr-xr-x 2000-11-21 19:02 +0100 725 fixsome
-rwxr-xr-x 2000-11-21 19:02 +0100 971 getenv
-rwxr-xr-x 2000-11-21 19:02 +0100 2683 install
-rwxr-xr-x 2000-11-21 19:02 +0100 1278 installfonts
-rwxr-xr-x 2000-11-21 19:02 +0100 2423 latex
-rwxr-xr-x 2000-11-21 19:02 +0100 1309 logo
-rwxr-xr-x 2000-11-21 19:02 +0100 448 make
-rwxr-xr-x 2000-11-21 19:02 +0100 743 makeall
-rwxr-xr-x 2000-11-21 19:02 +0100 3883 mkdir
-rwxr-xr-x 2000-11-21 19:02 +0100 650 nonascii
-rwxr-xr-x 2000-11-21 19:02 +0100 264 symbolinput
-rwxr-xr-x 2000-11-21 19:02 +0100 845 unsymbolize
-rwxr-xr-x 2000-11-21 19:02 +0100 3411 usedir