#1035 (Oct 18, 2019, 12:50:06 AM)

1. turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof; (detail / hgweb)
2. support dummy term; (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. proof boxes based on proof digest (not proof term): thus it works with prune_proofs; (detail / hgweb)
5. proper Thm.transfer; (detail / hgweb)
6. clarified files; (detail / hgweb)
7. clarified proof_boxes (requires prune_proofs=false); (detail / hgweb)
8. tuned; (detail / hgweb)
9. more robust; (detail / hgweb)

Started by an SCM change

This run spent:

• 5.3 sec waiting;
• 1 hr 21 min build duration;
• 1 hr 21 min total from scheduled to completion.