Changes

Summary

1. merged
2. proper ML names;
3. clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
4. some treatment of OfClass proofs;
5. tuned signature;
6. misc tuning and clarification;
7. proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
8. clarified oracle_proof;
9. tuned;
10. tuned;
11. tuned;
12. clarified signature;
13. tuned signature;
14. more compact XML representation;
15. proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
16. tuned;
17. tuned -- more direct ML expressions;
18. clarified modules;
19. tuned whitespace;
20. more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
21. unused;
22. document antiquotations + clarify porting text slightly