lib/Tools/unsymbolize
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2000-11-30 wenzelm 2000-11-30 /usr/bin/env bash;
2000-11-22 wenzelm 2000-11-22 tuned;
2000-09-18 wenzelm 2000-09-18 remove unreadable symbol names from sources;