isabelle update -u control_cartouches;

more symbols;

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

isabelle update_cartouches -c -t;

more symbols;

prefer tactics with explicit context;

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

proper context for assume_tac (atac remains as fall-back without context);

modernized header uniformly as section;

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

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

prefer Proof.context over old-style clasimpset;

modernized specifications;

updated some headers;

modernized specifications;

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

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

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

fixed imports from ../../Auth;

misc cleanup of ML bindings (for multihreading);

stripped some legacy bindings

simplified method setup;

added explicit paths to required theories

migrated theory headers to new format

local_cla/simpset_of;

conversion of NSP_Bad to Isar script

converting HOL/UNITY to use unconditional fairness

conversion of UNITY theories to new-style

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp