isabelle update -u control_cartouches;

clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;

tuned syntax -- more symbols;

fewer aliases for toplevel theorem statements;

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

more symbols;

simplifie sessions;

more Isar proof methods;

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

modernized header uniformly as section;

mark schematic statements explicitly;

removed old CVS Ids;
tuned headers;

allow non-trivial schematic goals (via embedded term vars);

removed obsolete ML files;