#2078 (Dec 19, 2023, 2:42:04 AM)

1. more thorough beta contraction;
   removed unused operations; (detail / hgweb)
2. tuned whitespace; (detail / hgweb)
3. tuned; (detail / hgweb)
4. more operations, following proofterm.ML; (detail / hgweb)
5. tuned; (detail / hgweb)
6. clarified signature, following Term.subst_bounds_same; (detail / hgweb)
7. tuned whitespace; (detail / hgweb)
8. minor performance tuning: more concise union; (detail / hgweb)
9. tuned comments; (detail / hgweb)
10. tuned, following close_proof; (detail / hgweb)
11. proper treatment of proof hyps, following 8368160d3c65; (detail / hgweb)
12. proper treatment of proof hyps: unchangeable, like bound; (detail / hgweb)
13. proper Thm.transfer (required for zproofs); (detail / hgweb)
14. clarified signature; (detail / hgweb)
15. proper beta_norm after instantiation (amending 90c5aadcc4b2); (detail / hgweb)
16. minor performance tuning: more direct beta_norm; (detail / hgweb)
17. more robust norm_proof: turn env into instantiation, based on visible statement; (detail / hgweb)
18. proper scope of cache (amending 61af3e917597); (detail / hgweb)
19. tuned comments; (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 52 min waiting;
• 2 hr 7 min build duration;
• 3 hr 59 min total from scheduled to completion.