isabelle update -u control_cartouches;

tuned signature -- prefer qualified names;

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

proper context for "net" tactics;
avoid implicit Tactic.build_net -- make its operational behavior explicit in application;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

do not open ML structures;

more antiquotations

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

fixed title

split off modal.ML from provers.ML