Changes

Summary

1. a generic horner sum operation
2. more thms
3. clarified message --- as in former ML version (see 940195fbb282);
4. clarified signature;
5. clarified messages: avoid duplicate Timing;
6. clarified messages;
7. clarified signature;
8. tuned;
9. avoid duplicate Timing messages (see also 5c4800f6b25a);
10. more accurate message;
11. tuned;
12. clarified signature;
13. clarified inlined protocol messages;
14. removed unused property;
15. signed_take_bit
16. more on single-bit operations