updated;

added internal_mode;

simplified abbrev: single argument;

TermSyntax.abbrev; ProofContext.set_expand_abbrevs;

added read/pretty_term_abbrev, print_abbrevs; tuned Consts signature; renamed expand_abbrevs to set_expand_abbrevs;

init_context: reset naming;

added 'print_abbrevs';

added print_abbrevs; exit: less verbosity;

added term_abbrev;

renamed reserved to reserved_names; added reserved: Name.context;

tuned Consts signature;

abbrevs: print original rhs;

abbreviate: always authentic, force expansion of internal abbreviations; tuned signature; tuned;

ML_Syntax.reserved(_names);

TermSyntax.abbrev;

added antiquotation abbrev;

added print_abbrevs;

tuned use_text; eval command line: skip over -q option;

added 'help' command (same of 'print_commands');

more careful evaluation of ML text, prevents spurious output;

date: forcing LC_ALL=C prevents funny file names;

root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);

patched up the proofs agsin

removed use of put_name_hint, as the ATP linkup no longer needs this

reorganized structure Tactic vs. MetaSimplifier;

begin/end blocks; tuned notation;

abbrevs: more careful interpretation, avoid dynamic references to local names;

definition/abbreviation: single argument;

simplified add_abbrev -- single argument;

removed obsolete references to ProofGeneral/isa;