Changes

Summary

1. updated to polyml-5.8.1-20191101 test version;
2. merged
3. more operations;
4. proper export of unnamed proof boxes for unnamed toplevel declarations, e.g. rulify/defn rules in theory IFOL and HOL;
5. clarified signature (again);
6. clarified signature;
7. make double-sure that internal proof boxes are exported, e.g. in Pure;
8. avoid redundant proof boxes for application sessions;
9. clarified modules (again);
10. more detailed proof term output; tuned signature;
11. tuned signature;
12. clarified error;
13. more accurate proof_boxes -- from actual proof body;
14. clarified signature;
15. clarified signature;