merged

proper orientation for right-associative operations;

tuned signature;

tuned signature;

tuned signature;

obsolete --- superseded by SHA1.Shasum operations;

clarified signature, using right-associative operation;

tuned whitespace;

tuned --- implicit split;

clarified signature;

prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;

tuned signature;

more uniform use of SHA1.Shasum;

proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types;

prefer explicit shasum; clarified signature;

proper symbolic dependencies, e.g. for Demo_FoilTeX;

prefer explicit shasum;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature;

Some more new material and some tidying of existing proofs

more diagnostic operations (see also 5c7652e9bc01);

more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);

tuned;

clarified modules;

tuned signature;

update to polyml-5e9c8155ea96, which is more robust on arm64;

more robust dependencies for Pure;

proper compiler root for arm64;