tuned syntax -- more symbols;

fewer aliases for toplevel theorem statements;

isabelle update_cartouches;

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

more symbols;

tuned whitespace;

simplifie sessions;

more Isar proof methods;

proper context for assume_tac (atac remains as fall-back without context);

modernized header uniformly as section;

more antiquotations;

mark schematic statements explicitly;

removed old CVS Ids;
tuned headers;

removed obsolete ML files;