Changes

Summary

1. Some new simprules – and patches for proofs
2. merged
3. tuned proofs; tuned whitespace;
4. merged, resoving conflicts in src/HOL/Nominal/Nominal.thy;
5. Added tag Isabelle2024-RC3 for changeset 007e6af8a020
6. more documentation on "System registry via TOML";
7. update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows;
8. provide 3.1 for testing (inactive);
9. build e-3.1, without patch;
10. disable Isabelle/Naproche for now: does not quite work on Windows;
11. update and activate naproche component for release;
12. changed URL to SystemOnTPTP at Geoff's request
13. tuned spelling;
14. build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state;
15. proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash;
16. support more Ubuntu versions;
17. updated for release;
18. more robust: avoid spurious ConcurrentModificationException;
19. update to e-3.0.03-1, with proper support for trivial statements;
20. more robust;
21. minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements;
22. backed out changeset 601ff5c7cad5: not relevant for Isabelle2024;
23. clone of 0c51e0a6bc37;
24. merged
25. update Windows test machines;
26. A little more tidying in Nominal
27. More tidying of proofs
28. Another Nominal example
29. merged
30. update Windows build host;
31. proper command-line;
32. Tidying up another Nominal example (SOS)
33. Tidying up another of the nominal examples
34. More tidying of Nominal proofs
35. Tidied up another messy theory
36. More proof tidying for Nominal
37. Tidying up more messy proofs
38. Starting to tidy HOL-Nominal-Examples
39. sketch & explore: recover from duplicate fixed variables in Isar proofs
40. back to post-release mode -- after fork point;
41. merged
42. Added tag Isabelle2024-RC2 for changeset ef2134570abb
43. Acknowledgement of Ata Keskin for his Martingales material
44. merged
45. update to jdk-21.0.3; enforce rebuild of Isabelle/ML and Isabelle/Scala;
46. merged
47. clarified signature;
48. make adhoc_overloading respect type constraints
49. merged
50. tuned;
51. clarified signature;
52. minor performance tuning: avoid redundant server access;
53. tuned;
54. clarified modules and options (from store);
55. clarified signature;
56. tuned;
57. clarified signature;
58. tuned signature;
59. tuned;
60. tuned signature;
61. tuned;
62. tuned;
63. more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
64. tuned messages;
65. tuned;
66. back to static numa_nodes (reverting part of c2c59de57df9);
67. tuned messages;
68. canonical time function for List.nth
69. Tidied up horrible archaic proofs
70. merged
71. clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
72. Streamlining of many more archaic proofs
73. More tidying of old proofs
74. merged
75. Add subgoals variant of 'sketch' command
76. More tidying and removal of "apply"
77. merged
78. prefer canonical theorem name for fact collection declarations
79. Tidied some messy proofs
80. merged
81. tuned;
82. Tidying ugly proofs