isabelle update_cartouches -c -t;

tuned whitespace;

tuned;

tuned syntax -- more symbols;

fewer aliases for toplevel theorem statements;

misc tuning;

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

modernized header uniformly as section;

more cartouches;

discontinued redundant ASCII syntax;

simplified/unified method_setup/attribute_setup;

mark schematic statements explicitly;

removed old CVS Ids;
tuned headers;

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

Removed debugging code.

Restructured locales with predicates: import is now an interpretation.
New method intro_locales.

plain test session, includes example;