Changes

Summary

1. clarified signature default;
2. clarified signature default;
3. more operations for type classes;
4. setup preprocessing for HOL proofs;
5. support preprocessing of exported proofs;
6. early setup of proof preprocessing;
7. clarified output and input of Typ/Term;
8. adapted to ML version;
9. more compact XML;
10. more compact XML: separate environment for free variables; clarified fold_proof_terms vs. fold_proof_terms_types;
11. more compact XML;