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;

added input_mode;

tuned print_locale output; add_decls: Thm.internalK;