isabelle update -u control_cartouches;

prefer tactics with explicit context;

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;

more uniform ML/document antiquotations;

more qualified names;

tuned signature;

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

tuned;

proper run-time context;

more system options as context-sensitive config options;

more conventional tactic setup;

prefer antiquotations;

more antiquotations;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;

expanded some aliases from structure Unsynchronized;

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

formerly unnamed infix impliciation now named HOL.implies

more antiquotations

use antiquotations for remaining unqualified constants in HOL

less pervasive names from structure Thm;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

explicit indication of Unsynchronized.ref;

qualified Subgoal.FOCUS;

FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;

eliminated METAHYPS;

more antiquotations;

pervasive RuleInsts;

ptac/prolog_tac: proper context;

Drule.read_instantiate;

HOL-Prolog: converted legacy ML scripts;