isabelle update -u control_cartouches;

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

prefer tactics with explicit context;

isabelle update_cartouches;

more symbols;
eliminated alternative syntax;

more symbols;

more symbols;

support 'for' fixes in rule_tac etc.;

tuned signature;

more position information;

tuned signature -- prefer qualified names;

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

modernized header uniformly as section;

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

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

tuned;

eliminated old 'axioms';

eliminated obsolete "standard";

new fastforce replacing fastsimp - less confusing name

simplified/unified method_setup/attribute_setup;

proper runtime context for auto_inv_tac;

clarified map_simpset versus Simplifier.map_simpset_global;

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

tuned proof;

proper method_setup;

removed obsolete old-style cs/css;

proper method_setup;

eliminated global prems;

modernized syntax/translations;
tuned headers;

modernized translations;

simplified attribute setup;

pervasive RuleInsts;

proper context for tactics derived from res_inst_tac;

avoid rebinding of existing facts;
proper ML antiquotations;

TLA: converted legacy ML scripts;

converted to Isar theory format;

use more symbols in HTML output

eliminated old "symbols" syntax, use "xsymbols" instead;

tuned version by Stephan Merz (unbatchified etc.);

tuned;

updated (Stephan Merz);

symbols syntax;

A formalization of TLA in HOL -- by Stephan Merz;