reverted to old version of Set.thy -- strange effects have to be traced first

simplified attribute and method setup;

simplified attribute setup; replaced add_args by add parser;

simplified attribute setup;

updated generated files;

added 'attribute_setup' command;

added setup and attribute_setup -- expect plain parser instead of syntax function; aded add_del parser;

ML_Syntax.make_binding;

added make_binding;

removed obsolete no_base_names naming policy;

merged

merged

coherent binding policy with primitive target operations

moved some generic nonsense to arith_data.ML

tuned ML code

remove legacy ML bindings

simplified method setup;

simplified goal_spec: default to first goal;

eliminated type Args.T; pervasive types 'a parser and 'a context_parser;

added simplified setup; eliminated type Args.T; pervasive types 'a parser and 'a context_parser;

pervasive types 'a parser and 'a context_parser;

unified type Proof.method and pervasive METHOD combinators;

more regular method setup via SIMPLE_METHOD;

tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;

merged

fix typed print translation for CARD('a)

introduce new helper functions; clean up proofs

merged

added comment

hiding numeric coercions in LaTeX