Changes

Summary

1. merged
2. tuned;
3. removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
4. just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);
5. proper version;
6. back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);
7. less ambitious parallelism: more direct read/write saves overall heap space and GC time;
8. slightly faster XML output: avoid too much regrowing of StringBuilder;
9. updated NEWS: arm64-linux support is almost complete;
10. update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;
11. more material for HOL-Analysis.Infinite_Sum
12. more symbolic latex_output via XML;
13. clarified signature;
14. updated to polyml-5.9-610a153b941d -- close to final;
15. tuned signature (again): latex_output is likely to depend on context;
16. more symbolic latex output; discontinued Latex.output_text, which is in conflict with symbolic output;
17. tuned signature;
18. symbolic latex_output via XML, interpreted in Isabelle/Scala;
19. tuned signature;
20. clarified signature;
21. clarified signature;
22. clarified signature: more privacy;
23. tuned output --- less redundancy;
24. tuned whitespace;
25. clarified signature: Latex.Output as parameter to Document_Build.Engine; tuned;
26. proper detection of ARM platform variants;