isabelle update -u control_cartouches;

eliminated old defs;

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

isabelle update_cartouches;

more symbols;
eliminated alternative syntax;

more symbols;

more symbols;

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;

more antiquotations;

prefer vacuous definitional type classes over axiomatic ones;

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

tuned signature -- depend on context by default;

eliminated old 'axioms';

simplified/unified method_setup/attribute_setup;

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

proper method_setup "enabled";

modernized specifications;

"prod" and "sum" replace "*" and "+" respectively

observe standard convention for syntax consts;

dropped axclass, going back to purely syntactic type classes

modernized syntax/translations;
tuned headers;

simplified attribute setup;

rep_datatype command now takes list of constructors as input arguments

tuned ML setup;

TLA: converted legacy ML scripts;

converted to Isar theory format;

tuned;

tuned version by Stephan Merz (unbatchified etc.);

updated (Stephan Merz);

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