Changes

Summary

1. tuned -- slightly smaller future closure size;
2. clarified menu actions;
3. purge history more thoroughly (see also 3156faac30a7);
4. merged
5. type class generalisations; some work on infinite products
6. merged
7. simplified some messy proofs
8. clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); tuned headers;