Removed needless quotes

removed bash debug;

removed -r option; added -p option;

fixed -m order;

improved xterm, xterm_color;

added comment;

added comment: print translations do not mark tokens;

added color styles; refs for test;

improved err msg;

*** empty log message ***

more robust handling of invocation errors; added -m MODE option;

more robust handling of invocation errors;

now uses -m symbols;

split ast_of_term(T); ast_of_term now marks frees; added token translation support;

added token translation support;

term_of_... now mark class, tfree, tvar;

added mark_bound(T), variant_abs'; trfuns now mark bounds they introduce!! added pure_trfunsT;

Token translations for xterm and LaTeX output.

added _mk_ofclass(S);

added strlen (includes metric information); removed map_strs;

added token_translation interface;

added add_tokentrfuns;

added Syntax/token_trans.ML;

added token_trans.ML;

Slightly more robust proof

dup_intr & dup_elim no longer call standard -- this lets them be used on meta-hyps

rule_by_tactic no longer standardizes its result

Addition of de Bruijn formulae

tuned comment;

tuned comments;