session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
eliminated old defs;
isabelle update_cartouches;
more symbols; eliminated alternative syntax;
more symbols;
modernized header uniformly as section;
tuned headers;
TLA: converted legacy ML scripts;
converted to Isar theory format;
updated (Stephan Merz);
A formalization of TLA in HOL -- by Stephan Merz;