isabelle update_cartouches -c -t;

prefer local fixes;

modernized header uniformly as section;

tuned context specifications and proofs;

prefer high-level elim_format;

tuned proofs;

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;

misc cleanup of ML bindings (for multihreading);

migrated theory headers to new format

minor revisions

converting HOL/UNITY to use unconditional fairness

conversion to new-style theories and tidying

converting UNITY to new-style theories

added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.

abolition of localTo: instead "guarantees" has local vars as extra argument

working again; new treatment of LocalTo

exchanged the first two args of "project" and "drop_prog"

working version with localTo[C] instead of localTo

working shapshot with "projecting" and "extending"

working snapshot (even Alloc)

working snapshot with new theory "Project"