#2072 (Dec 7, 2023, 5:40:15 AM)

1. tuned structure; (detail / hgweb)
2. tuned; (detail / hgweb)
3. merged (detail / hgweb)
4. performance tuning: cache for ztyp_of within zterm_of;
   clarified signature; (detail / hgweb)
5. tuned names; (detail / hgweb)
6. minor performance tuning; (detail / hgweb)
7. more zproofs; (detail / hgweb)
8. minor performance tuning; (detail / hgweb)
9. tuned; (detail / hgweb)
10. more zproofs; (detail / hgweb)
11. clarified modules; (detail / hgweb)
12. more zproofs; (detail / hgweb)
13. more zproofs; (detail / hgweb)
14. proper treatment of ZConstP: term represents body of closure; (detail / hgweb)
15. proper substitution of types within term; (detail / hgweb)
16. more accurate treatment of term variables after instantiation of type variables; (detail / hgweb)
17. tuned signature; (detail / hgweb)
18. tuned; (detail / hgweb)
19. check that Isar proofs contain one 'show' (detail / hgweb)
20. include unnamed chained facts in Sledgehammer's relevance filter (detail / hgweb)
21. merge (detail / hgweb)
22. removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics (detail / hgweb)
23. don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts (detail / hgweb)
24. tuned T functions: now 0 if not recursive (detail / hgweb)
25. minor performance tuning; (detail / hgweb)
26. tuned; (detail / hgweb)
27. more zproofs;
    clarified signature; (detail / hgweb)
28. misc tuning and clarification;
    eliminate clones (see also 3ae09d27ee7a); (detail / hgweb)
29. more zproofs; (detail / hgweb)
30. more operations; (detail / hgweb)
31. more operations; (detail / hgweb)
32. tuned; (detail / hgweb)
33. clarified signature; (detail / hgweb)
34. more zproofs; (detail / hgweb)
35. more ML pretty-printing; (detail / hgweb)
36. clarified const_proof vs. zproof_name; (detail / hgweb)

Started by an SCM change

This run spent:

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