#2085 (Dec 27, 2023, 1:47:27 AM)

1. proper Thm.trim_context; (detail / hgweb)
2. clarified stored data: actual thm allows to replay zproofs in a modular manner; (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. tuned signature, following Proofterm.thm_header; (detail / hgweb)
5. more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata; (detail / hgweb)
6. clarified signature; (detail / hgweb)
7. proper Thm_Name.make_list for thm_definition;
   tuned modules; (detail / hgweb)

Started by an SCM change

This run spent:

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