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;

simplified ML bindings;

simplified ML bindings -- moved to HOL.thy; removed confusing simpset_basic/simplify;

added basic ML bindings;

added aliases for nat_recs/cases;

removed legacy ML bindings; simplified ML setup; tuned declarations;

reduced to genuine legacy bindings -- others in HOL.thy;

removed legacy ML bindings;

target_name: allow qualified names;

add_notation: permissive about undeclared consts; add_abbrevs: allow qualified names; tuned;

generic_goal: enable stmt mode;

encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;

notation/abbreviation: more serious handling of morphisms;

print_syntax etc.: plain Toplevel.context_of;

attribute value: morphism;

add_notation: permissive about undeclared consts;

added mapping_result;

added ML-Systems/polyml-5.0.ML;

Attrib.internal: morphism;

removed duplicate abbreviations (implicit inheritance);

restored notation for less/less_eq (observe proper order of mixfix annotations!); simplified notation for greater/greater_eq, which is only used for input; removed duplicate abbreviations (implicit inheritance);