session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

setsum -> sum

instantiate multiset with multiset ordering

isabelle update_cartouches -c -t;

more succint formulation of membership for multisets, similar to lists;
discontinued ASCII notation for multiset membership;
more theorems on multisets, dropping redundant interpretation;
modernized notation;
some annotations concerning future work

tuned proofs -- less legacy;

eliminated \<Colon>;

Renaming multiset operators < ~> <#,...

modernized header uniformly as section;

generalized and strengthened cong rules on compound operators, similar to 1ed737a98198

prefer abstract simp rule

explicit file specifications -- avoid secondary load path;

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

tuned proofs

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

tuned proof; tuned headers

patched up the proofs agsin

migrated theory headers to new format

new simprules Int_subset_iff and Un_subset_iff

converting HOL/UNITY to use unconditional fairness

some x-symbols

conversion to new-style theories and tidying

converting more UNITY theories to new-style

use Multiset from HOL/Library;

new parent MultisetOrder and new results about multiset unions

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

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.

Working version after a FAILED attempt to base Follows upon LeadsETo

shortened Follows to Fols

Theory of the "Follows" relation