more symbols;

isabelle update_cartouches -c -t;

prefer abbreviations for compound operators INFIMUM and SUPREMUM

prefer symbols for "Union", "Inter";

discontinued ASCII replacement syntax <*>;

discontinued ASCII replacement syntax <->;

prod_case as canonical name for product type eliminator

modernized header uniformly as section;

tuned context specifications and proofs;

tuned proofs;

Replace surj by abbreviation; remove surj_on.

modernized specifications;

inv_onto -> inv_into

Inv -> inv_onto, inv abbr. inv_onto UNIV.

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

migrated theory headers to new format

minor revisions

converting HOL/UNITY to use unconditional fairness

some x-symbols

conversion to new-style theories and tidying

converting UNITY to new-style theories

*** empty log message ***

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

restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML

Times -> <*>
** -> <*lex*>

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

working version with localTo[C] instead of localTo

working shapshot with "projecting" and "extending"

project_act no longer has a special case to allow identity actions

working snapshot

working snapshot

changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <

use of bij, new theorems, etc.

project constants

made definition more readable

new theory of extending the state space