Changes

Summary

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