Changes

Summary

1. merged
2. use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
3. clarified signature: let Sledgehammer handle SystemOnTPTP comments;
4. clarified signature: url may change dynamically and is part of result;
5. clarified error;
6. support timeout, similar to perl LWP::UserAgent;
7. clarified signature;
8. tuned;
9. clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
10. support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
11. clarified HTTP.Content: support encoding; more realistic HTTP.Client operations;
12. clarified signature: more explicit HTTP operations;
13. tuned;
14. more robust;
15. clarified signature;
16. clarified components;
17. avoid name clash
18. lemma
19. tuned;
20. another example for lift_bnf for quotients
21. merged
22. proper \usepackage[T1]{fontenc};
23. more robust init: avoid spilling opam artifacts;
24. proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
25. provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
26. more robust; eliminated perl;
27. removed unused latex packages;
28. obsolete (see 0c837beeb5e7);
29. proper Isabelle/Scala tool --- avoid perl;
30. generalized confluence-based subdistributivity theorem for quotients; new example that triggered the generalization
31. Backed out changeset 3fdb94d87e0e
32. Backed out changeset b867b436f372
33. reduced dependencies on List_Permutation
34. follow corresponding precedence on sets
35. consolidated names
36. reduced dependencies on theory List_Permutation

Summary

1. avoid name clash
2. adapted to LuaLaTeX according to Isabelle/299f6a8faccc; \usepackage[T1]{fontenc} is default, it provides e.g. proper cartouche-delimiters; \usepackage{lmodern} is no longer required, since T1 in LuaLaTeX has proper scalable fonts; \usepackage[utf8]{inputenc} is obsolete in LuaLaTeX; tuned whitespace;
3. reduced dependencies on List_Permutation
4. follow corresponding precedence on sets
5. consolidated names
6. reduced dependencies on theory List_Permutation