simplified/unified command setup;

removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;

prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;

tuned eval_thms (cf. note etc. in proof.ML);

use Pretty.enum convenience;

tuned whitespace;

more precise and more maintainable dependencies;

merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;

* -> prod

added .ML extension

avoid old unnamed infix

avoid inclusion of Natural module in generated code

explicit ML extension

merged

separate initialisation for overloading and instantiation target

different foundations for different targets; simplified syntax handling of abbreviations

deleted duplicate lemma

Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.

basic renumbering

avoiding redundant primes

separated type from term parameters

moved extra_tfrees check for mixfix syntax to Generic_Target

name and argument grouping tuning

whitespace tuning

added generic_target.ML

try to uniformly follow define/note/abbrev/declaration order as close as possible

split off structure Generic_Target into separate file

split off generic parts of target implementations into separate structure

restructured code for `declaration`