#2203 (Jun 10, 2024, 4:02:22 AM)

1. merged (detail / hgweb)
2. clarified data representation: prefer explicit type Thm_Name; (detail / hgweb)
3. more operations, following Isabelle/ML; (detail / hgweb)
4. clarified signature: more explicit operations; (detail / hgweb)
5. clarified treatment of Thm_Name.T (again, see also 8a9588ffc133); (detail / hgweb)
6. clarified operations, including exceptions; (detail / hgweb)
7. tuned: more direct Isabelle/ML; (detail / hgweb)
8. clarified modules; (detail / hgweb)
9. more accurate thm "name_hint", using Thm_Name.T; (detail / hgweb)
10. more operationsd; (detail / hgweb)
11. tuned; (detail / hgweb)
12. more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms); (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. clarified output, following Consumer_Thread.failure; (detail / hgweb)
15. more informative exception output, with optional trace; (detail / hgweb)
16. more accurate output of Thm_Name.T wrt. facts name space; (detail / hgweb)
17. clarified signature: more operations; (detail / hgweb)
18. tuned structure; (detail / hgweb)
19. tuned; (detail / hgweb)
20. more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name; (detail / hgweb)
21. clarified signature: prefer explicit operation; (detail / hgweb)
22. clarified signature; (detail / hgweb)
23. tuned: prefer Thm_Name operations; (detail / hgweb)
24. tuned; (detail / hgweb)
25. prefer dynamic position from command transaction; (detail / hgweb)
26. tuned signature; (detail / hgweb)
27. clarified signature: more explicit preprocessing; (detail / hgweb)
28. clarified signature: separate formal context from exported theory_name; (detail / hgweb)
29. tuned signature: just one ZThm is sufficient; (detail / hgweb)

Started by an SCM change

This run spent:

• 3 hr 12 min waiting;
• 2 hr 2 min build duration;
• 5 hr 14 min total from scheduled to completion.