Added splicing algorithm.

hide (open) const;

simplified AxClass.add_axclass interface;

added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;

removed unused class_le_path, sort_less;

add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;

Term.itselfT;

Added function "splice"

Even/Odd: avoid clash with even/odd of Main HOL;

results: smart_pretty_thm uses adhoc proof context if possible;

added full_name; abbrevs: mode does not affect name space;

add_syntax: actually observe print mode;

print_term etc.: actually observe print mode in final output;

abbrevs: mode does not affect name space;

added coalesce;

moved theory presentation to Isar/ROOT.ML;

hide consts in Numeral.thy;

tuned syntax/abbreviations;

unfold(ed): not necessrily meta equations;

Made "empty" an abbreviation.

*** empty log message ***

Removed old set interval syntax.

pretty_term: late externing of consts (support authentic syntax);

pretty: late externing of consts (support authentic syntax);

removed fix_mixfix; added const_mixfix, mixfix_const;

abbreviation(_i): do not expand abbreviations, do not use derived_def;

add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;

abbrevs: support print mode;

simplified handling of authentic syntax (cf. early externing in consts.ML); simplified extern_term;

'abbreviation': optional print mode;