Changes

Summary

1. merged
2. support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);
3. tuned;
4. tuned: more parallel;
5. clarified modules;
6. clarified modules;
7. tuned;
8. tuned;
9. tuned signature;
10. tuned: more accurate transfer;
11. store facts as lazy values;
12. clarified operations;
13. misc tuning and clarification;
14. clarified signature;
15. clarified modules;
16. more operations;
17. added lemma