actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

merged

More new theorems from the number theory development

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;