Changes

Summary

1. merged
2. proper orientation for right-associative operations;
3. tuned signature;
4. tuned signature;
5. tuned signature;
6. obsolete --- superseded by SHA1.Shasum operations;
7. clarified signature, using right-associative operation;
8. tuned whitespace;
9. tuned --- implicit split;
10. clarified signature;
11. prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;
12. tuned signature;
13. more uniform use of SHA1.Shasum;
14. proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types;
15. prefer explicit shasum; clarified signature;
16. proper symbolic dependencies, e.g. for Demo_FoilTeX;
17. prefer explicit shasum;
18. clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
19. clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
20. clarified signature;
21. Some more new material and some tidying of existing proofs