clarified signature: make dynamic Queue from static Context;

clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;

tuned;

tuned;

clarified data structure: use static info from deps, not dynamic results; tuned;

clarified data structure: more direct access to timeout;

tuned;

misc tuning and clarification;

clarified modules; clarified signature;

tuned message: old_time not sufficiently prominent nor accurate to be printed;

clarified signature and terminology;

clarified signature: avoid adhoc constants;

tuned;

tuned message;

tuned signature: more operations;

clarified signature: more explicit types;

clarified modules;

clarified signature;

clarified signature;

merged

Simplification of proofs

explicit range types in abstractions

somehow more clear terminology

tuned

Some basis results about trigonometric functions

merged

Even more new material from Eberl and Li

merged

More material for Analysis and Complex_Analysis

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;