Changes

Summary

1. tuned signature;
2. prefer ctyp operations;
3. meson: more cterm operations;
4. more ctyp operations;
5. tuned;
6. clarified: use existing Thm.dest_ctyp_fun (which is more strict);
7. prefer exception TYPE, e.g. when used within conversion;
8. tuned signature -- more ctyp operations;
9. clarified group of "main" library sessions;
10. tuned signature -- more ctyp operations;
11. merged
12. tuned signature: more operations;
13. backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
14. tuned
15. more document structure
16. tuned
17. more abbrevs;
18. obsolete;