#914 (Jun 9, 2024, 10:56:04 PM)

Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

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

Started by an SCM change

This run spent:

• 2 min 2 sec waiting;
• 1 min 23 sec build duration;
• 3 min 26 sec total from scheduled to completion.

• refs/remotes/origin/master