Changes

Summary

1. merged
2. clarified signature;
3. clarified signature;
4. tuned signature;
5. tuned;
6. clarified test: no exception yet;
7. tuned;
8. tuned;
9. tuned signature: more direct operations;
10. clarified signature;
11. clarified signature: more direct operations;
12. tuned signature;
13. tuned;
14. minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
15. tuned whitespace;
16. more robust: certify types uniformly (see also 62b75508eb66);
17. tuned;
18. clarified signature;
19. clarified signature: avoid redundant Term.maxidx_of_term;
20. proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
21. misc tuning and clarification: prefer Same.operation;
22. clarified signature;
23. tuned names;
24. clarified signature;
25. tuned whitespace;
26. clarified modules; minor performance tuning;
27. clarified signature;
28. added and removed lemmas
29. proper SMTP session: set envelope sender address correctly;