isabelle update -u control_cartouches;

more symbols;

isabelle update_cartouches -c -t;

prefer tactics with explicit context;

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

modernized header uniformly as section;

uniform Proof.context for hyp_subst_tac;

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

eliminated obsolete "standard";

new fastforce replacing fastsimp - less confusing name

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

updated some headers;

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

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

sources are not executable;

tuned ML bindings (for multithreading);

Adapted to new inductive definition package.

simplified method setup;

tactic/method simpset: maintain proper context;

new and updated protocol proofs by Giamp Bella