#2080 (Dec 21, 2023, 2:15:10 AM)

1. proper Thm.transfer; (detail / hgweb)
2. clarified context: avoid capture of thy2 within closure; (detail / hgweb)
3. tuned names; (detail / hgweb)
4. more informative exceptions; (detail / hgweb)
5. more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy"); (detail / hgweb)
6. tuned; (detail / hgweb)
7. more informative exception; (detail / hgweb)
8. clarified signature; (detail / hgweb)
9. clarified ML toplevel output: avoid "??." prefix; (detail / hgweb)
10. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 25 min waiting;
• 2 hr 6 min build duration;
• 3 hr 31 min total from scheduled to completion.