#626 (Dec 16, 2016, 8:22:05 PM)

1. merged (detail / hgweb)
2. consolidate nested thms with persistent result, for improved performance;
   always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d; (detail / hgweb)
3. tuned signature -- more abstract type thm_node; (detail / hgweb)
4. tuned signature; (detail / hgweb)
5. tuned; (detail / hgweb)
6. back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738); (detail / hgweb)
7. simplified options; (detail / hgweb)
8. more careful derivation_closed / close_derivation; (detail / hgweb)
9. always close derivation, for significantly improved performance without parallel proofs; (detail / hgweb)
10. tuned whitespace; (detail / hgweb)
11. removed of_string_limited; (detail / hgweb)
12. tuned; (detail / hgweb)
13. tuned; (detail / hgweb)
14. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

• 5 min 1 sec waiting;
• 1 hr 27 min build duration;
• 1 hr 32 min total from scheduled to completion.