isabelle update_cartouches;

modernized header uniformly as section;

modernized specifications;

tuned headers;

TLA: converted legacy ML scripts;

converted to Isar theory format;

migrated theory headers to new format

tuned;

updated (Stephan Merz);

A formalization of TLA in HOL -- by Stephan Merz;