Changes

Summary

1. more thorough beta contraction; removed unused operations;
2. tuned whitespace;
3. tuned;
4. more operations, following proofterm.ML;
5. tuned;
6. clarified signature, following Term.subst_bounds_same;
7. tuned whitespace;
8. minor performance tuning: more concise union;
9. tuned comments;
10. tuned, following close_proof;
11. proper treatment of proof hyps, following 8368160d3c65;
12. proper treatment of proof hyps: unchangeable, like bound;
13. proper Thm.transfer (required for zproofs);
14. clarified signature;
15. proper beta_norm after instantiation (amending 90c5aadcc4b2);
16. minor performance tuning: more direct beta_norm;
17. more robust norm_proof: turn env into instantiation, based on visible statement;
18. proper scope of cache (amending 61af3e917597);
19. tuned comments;