#208 (Dec 17, 2016, 12:50:09 AM)

1. refactored induction principle generation code, for reuse for nonuniform datatypes (detail / hgweb)
2. merged (detail / hgweb)
3. 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)
4. tuned signature -- more abstract type thm_node; (detail / hgweb)
5. tuned signature; (detail / hgweb)
6. tuned; (detail / hgweb)
7. back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738); (detail / hgweb)
8. simplified options; (detail / hgweb)
9. more careful derivation_closed / close_derivation; (detail / hgweb)
10. always close derivation, for significantly improved performance without parallel proofs; (detail / hgweb)
11. tuned whitespace; (detail / hgweb)
12. removed of_string_limited; (detail / hgweb)
13. tuned; (detail / hgweb)
14. tuned; (detail / hgweb)
15. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

• 7.4 sec waiting;
• 1 hr 6 min build duration;
• 1 hr 7 min total from scheduled to completion.