isabelle update -u control_cartouches;

eliminated old defs;

isabelle update_cartouches -c -t;

isabelle update_cartouches;

prefer tactics with explicit context;

misc tuning;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

more symbols;

tuned whitespace;

more Isar proof methods;

modernized header uniformly as section;

tuned signature -- rearranged modules;

syntax translations always depend on context;

simplifier uses proper Proof.context instead of historic type simpset;

simplified/unified method_setup/attribute_setup;

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

proper antiquotations;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

modernized specifications -- less axioms;

eliminated global prems;

more antiquotations;

more antiquotations;
eliminated legacy ML bindings;

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

modernized some syntax translations;

misc modernization: proper method setup instead of adhoc ML proofs;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

more antiquotations;

eliminated global SIMPSET, CLASET etc. -- refer to explicit context;

proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);

more antiquotations;

avoid unnamed infixes;
tuned;

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

removed obsolete ML files;

replaced _K by dummy abstraction;

converted to Isar theory format;

proper use of 'syntax';

fixed dots;

expanded tabs

Gave tighter priorities to SUM and PROD to reduce ambiguities.

added parse rules for -> and *;
removed ndependent_tr;

Initial revision