isabelle update -u control_cartouches;

Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.

ran isabelle update_op on all sources

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;

optional proof context for unify operations, for the sake of proper local options;

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;

simplified/unified method_setup/attribute_setup;

modernized specifications;

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

formerly unnamed infix impliciation now named HOL.implies

use antiquotations for remaining unqualified constants in HOL

observe standard convention for syntax consts;

dropped axclass, going back to purely syntactic type classes

modernized syntax/translations;
tuned headers;

structure Thm: less pervasive names;

Set.insert with authentic syntax

simplified attribute setup;

tuned ML setup;

TLA: converted legacy ML scripts;

Adapted to changes in FixedPoint theory.

converted to Isar theory format;

use more symbols in HTML output

renamed class "term" to "type" (actually "HOL.type");

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

tuned version by Stephan Merz (unbatchified etc.);

'a list: Nil, Cons;

HTML output;

updated (Stephan Merz);

symbols syntax;

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