Changes

Summary

1. provide bash_process server for Isabelle/ML and other external programs; clarified signature for Bash.params;
2. clarified signature;
3. clarified signature;
4. proper prover_options for batch-build;
5. clarified signature; clarified errors;
6. clarified signature: more options for bash_process;
7. tuned signature;
8. clarified signature;
9. clarified signature;
10. follow phabricator 2021 Week 26; follow arcanist 2021 Week 23;
11. tuned signature;
12. tuned;
13. clarified signature;
14. clarified signature;
15. unused;
16. clarified signature;
17. merged
18. clarified modules;
19. type classes for XML data representation;
20. tuned signature;
21. clarified types: prefer Isabelle byte strings;
22. merged
23. added option labels to Mirabelle actions
24. more operations: dest binders;
25. clarified abstract and concrete boolean algebras
26. antiquotation for bundles
27. prefer persistent hash code for cachable items (see also 72b13af7f266);
28. merged
29. more operations: record overall exported entities;
30. merged
31. added dummy_fof prover to Sledgehammer
32. fixed malconfigured option output_dir in mirabelle
33. merged
34. clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
35. proper name space "kind": this is a formal name, not comment;
36. more uniform signatures in ML and Scala;
37. merged
38. fixed typo
39. added dummy_thf prover to Sledgehammer
40. simplified hierarchy of type classes for bit operations
41. obsolete
42. more operations, notably free and bound variables as in Isabelle/Pure;
43. more operations on types and terms; abstract syntax operations for Pure and HOL;
44. clarified jEdit java sources;
45. clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons;
46. removed junk;
47. moved theory Bit_Operations into Main corpus
48. more operations;
49. clarified signature;
50. clarified signature;
51. organize syntax for word operations in bundles
52. support for Lazy.Text;
53. prefer compact Isabelle.Bytes;
54. clarified signature;
55. clarified signature --- more operations;
56. tuned;
57. clarified order of modules;
58. more operations;
59. tuned;

Summary

1. metadata update for MFMC_Countable
2. derive rel_pmf characterization from bounded and unbounded MFMC theorem
3. merged
4. drop boundedness requirement for the sink
5. avoid global tmp file: pointless due to implicit theory export;
6. repaired syntax
7. tuned signature, following Isabelle/d030b988d470;
8. generalized gt_rat_sign_change to square-free polynomials
9. minor updates to bibliography
10. clarified signature;
11. clarified abstract and concrete boolean algebras
12. antiquotation for bundles
13. simplified hierarchy of type classes for bit operations
14. restored executable conversions
15. dropped junk
16. moved theory Bit_Operations into Main corpus
17. organize syntax for word operations in bundles
18. more systematic approach for instantiation
19. avoid seemingly unused transfer rules