#2086 (Dec 28, 2023, 3:46:53 AM)

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

Started by an SCM change

This run spent:

• 2 hr 56 min waiting;
• 2 hr 4 min build duration;
• 5 hr 1 min total from scheduled to completion.