Changes

Summary

1. tuned proofs -- prefer explicit names for facts from 'interpret';
2. merged
3. eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
4. tuned signature;
5. tuned;
6. use lazy notes for locale context init and later additions of facts;
7. avoid premature Lazy.force due to strict "?" operator;
8. Merge
9. Merge
10. lots of new material, ultimately related to measure theory