#1941 (Apr 23, 2023, 1:53:37 AM)

1. tuned: concise combinators instead of bulky case-expressions; (detail / hgweb)
2. provide ML antiquotation "if_none": non-strict version of "the_default"; (detail / hgweb)
3. merged (detail / hgweb)
4. proper Thm.trim_context / Thm.transfer (see also 0d401f874942); (detail / hgweb)
5. tuned; (detail / hgweb)
6. more operations; (detail / hgweb)
7. more operations; (detail / hgweb)
8. more uniform operations wrt. Thm.full_prop_of; (detail / hgweb)
9. proper Thm.trim_context / Thm.transfer for context data; (detail / hgweb)
10. tuned: more concise data record; (detail / hgweb)
11. tuned; (detail / hgweb)
12. clarified counters and types; (detail / hgweb)
13. tuned signature; (detail / hgweb)
14. support n-ary merge theory data;
    less redundant use of ids and stages; (detail / hgweb)
15. tuned; (detail / hgweb)
16. tuned; (detail / hgweb)
17. proper theory_long_name; (detail / hgweb)
18. prefer theory_long_name in data; (detail / hgweb)
19. proper theory_long_name; (detail / hgweb)
20. clarified signature: explicitly distinguish theory_base_name vs. theory_long_name; (detail / hgweb)
21. tuned; (detail / hgweb)
22. more operations, following Isabelle/ML conventions; (detail / hgweb)
23. clarified theory_id: plain value without state; (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 3 min waiting;
• 2 hr 16 min build duration;
• 3 hr 20 min total from scheduled to completion.