Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

1. merged
2. clarified data representation: prefer explicit type Thm_Name;
3. more operations, following Isabelle/ML;
4. clarified signature: more explicit operations;
5. clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);
6. clarified operations, including exceptions;
7. tuned: more direct Isabelle/ML;
8. clarified modules;
9. more accurate thm "name_hint", using Thm_Name.T;
10. more operationsd;
11. tuned;
12. more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms);
13. clarified signature;
14. clarified output, following Consumer_Thread.failure;
15. more informative exception output, with optional trace;
16. more accurate output of Thm_Name.T wrt. facts name space;
17. clarified signature: more operations;
18. tuned structure;
19. tuned;
20. more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
21. clarified signature: prefer explicit operation;
22. clarified signature;
23. tuned: prefer Thm_Name operations;
24. tuned;
25. prefer dynamic position from command transaction;
26. tuned signature;
27. clarified signature: more explicit preprocessing;
28. clarified signature: separate formal context from exported theory_name;
29. tuned signature: just one ZThm is sufficient;