Changes

Summary

1. clarified global theory context;
2. more robust export, based on reconstruct_proof / expand_proof;
3. clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
4. tuned -- fewer warnings;
5. discontinued pointless messages;
6. clarified context;
7. clarified modules;
8. discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;