more symbols;

isabelle update_cartouches -c -t;

prefer abbreviations for compound operators INFIMUM and SUPREMUM

prefer symbols for "Union", "Inter";

prefer local fixes;

modernized header uniformly as section;

tuned context specifications and proofs;

tuned proofs;

tuned proofs;

eliminated obsolete "standard";

tuned proofs

modernized specifications;

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

Adapted to encoding of sets as predicates

tuned proof

Adapted to new inductive definition package.

migrated theory headers to new format

restored some deleted lemmas

minor revisions

converting HOL/UNITY to use unconditional fairness

conversion to new-style theories and tidying

converting UNITY to new-style theories

*** empty log message ***

quantifiers now allowed in inductive defs

still working; a bit of polishing

working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.

removing the "{} : CC" requirement for leadsTo[CC]

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

new generalized leads-to theory