Changes

Summary

1. clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;
2. tuned;
3. tuned signature;
4. tuned; more uniform Thm.transfer;
5. tuned;
6. more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
7. clarified modules;
8. clarified signature;
9. tuned;
10. clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
11. clarified signature;
12. tuned;
13. tuned: avoid duplicates;
14. more operations;
15. proper Thm.transfer;