removed obsolete references to ProofGeneral/isa;

added input_mode;

tuned print_locale output; add_decls: Thm.internalK;

moved notation/abbrevs to TermSyntax;

expand_term: based on Envir.expand_term; tuned;

thms etc.: proper treatment of internal_fact with selection;

tuned pretty_src output;

simplified add_abbrevs: no mixfix;

added expand_term;

tuned;

Common term syntax declarations.

added Isar/term_syntax.ML;

TermSyntax.notation/abbrevs;

Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.

Removal of theorem tagging, which the ATP linkup no longer requires,

Poly/ML 5.0 setup for Isabelle2005.

reorganized structure Goal vs. Tactic;

export: added explicit term operation;

abbrevs: actually observe target_morphism;

added expand; export: added explicit term operation;

moved hidden_polymorphism to term.ML;

added hidden_polymorphism (from variable.ML);

add_abbrevs: moved common parts to consts.ML;

abbreviate: improved error handling, return result;

export: added explicit term operation; tuned export_morphism -- lean closure;

LocalDefs.expand;

Improved tracing

no timing;