Changes

Summary

1. tuned text;
2. recover NEWS from 78d1f73bbeaa;
3. save 90 MB by excluding rlwrap and thus perl;
4. save 45 MB by excluding rlwrap and thus perl;
5. NEWS;
6. clarified test of directories;
7. misc tuning for release;
8. merged
9. updated to kodkodi-1.5.7. with more robust/portable management of files and processes;
10. provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick;
11. tuned message;
12. proper build on macOS;
13. build minisat, using recent fork from original sources;
14. proper platform_path for executables run from Java;
15. tuned message;
16. tuned;
17. tuned whitespace;
18. merged
19. added timeout to veriT
20. new notion of infinite sums in HOL-Analysis, ordering on complex numbers
21. NEWS and CONTRIBUTORS
22. merged
23. added offset to Mirabelle's tptp output names
24. tuned zipperposition config in sledgehammer
25. considered slices overhead in sledgehammer
26. tuned atp_prover sliding
27. tuned Zipperposition slides in sledgehammer
28. include arm64-linux;
29. updated to Vampire 4.6, as proposed by Martin Desharnais;
30. build from official downloads;
31. build just one vampire version;
32. clarified signature;
33. maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche;
34. more exports, notably for Isabelle/Naproche;
35. include arm64-linux;
36. prefer existing OCaml installation;
37. include arm64-linux;
38. no patchelf on macOS (undetected due to cached executables?);
39. provide opam-2.1.0 for experimentation;
40. rebuild cygwin-20211004.tar.gz;
41. include arm64-linux;
42. updated to cygwin-20211004: build again;
43. merged
44. removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default;
45. actually use cygwin-20211002 (amending ff0ca375457c);
46. discontinued perl;
47. clarified signature;
48. proper term operation Term.dest_abs;
49. tuned;
50. tuned proofs; fewer warnings;
51. more standard binder syntax;
52. clarified 'let' syntax: avoid conflict with existing 'let' in FOL;
53. tuned;
54. tuned;
55. merged
56. removal of a redundant theorem (and white space)
57. new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
58. clarified and updated for release;
59. formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;
60. more NEWS and CONTRIBUTORS;
61. clarified comments;
62. support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);
63. clarified dependencies;
64. updated for release;
65. Added tag Isabelle2021-1-RC0 for changeset fedc0b659881
66. provide Isabelle/jEdit plugins as services, and thus allow user components do the same;
67. merged
68. updated for release;
69. misc tuning for release;
70. update dependency;
71. trim whitespace;
72. misc tuning for release;
73. misc tuning for release;
74. isabelle build_components -u;
75. updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7;
76. updated to current Cygwin, near 3.2.0; discontinued perl;
77. updated to sumatra_pdf-3.3.3;
78. updated default version;
79. updated to xz-java-1.9;
80. updated to sqlite-jdbc-3.36.0.3;
81. updated to postgresql-42.2.24;
82. updated to jfreechart-1.5.3;
83. updated to flatlaf-1.6;
84. clarified signature;
85. clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;
86. clarified sledgehammer_provers, following d8dc8fdc46fc;
87. proper term operation Term.dest_abs;
88. tuned, following Syntax_Trans.variant_abs;
89. proper patterns for (- numeral t), amending 03ff4d1e6784;
90. tuned;
91. merged
92. update syntax for verit
93. clarified antiquotations;
94. clarified antiquotations;
95. provide verit-2021.06-rmx;

Summary

1. ETTS: minor amendments
2. CTR and ETTS: integration with fd5f62176987
3. adapted QHLProver to isabelle-dev/409ca22dee4c
4. adapted to isabelle-dev/409ca22dee4c
5. adapted to devel
6. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5
7. Weighted_Path_Order: update to isabelle@ffb15f7f26d5
8. merge from afp-2021
9. add missing session dependency
10. new entry FOL_Axiomatic
11. regen website
12. minor editorial changes for CZH entries
13. New entry Weighted_Path_Order
14. fxed metadata (forgot .html) in link
15. metadata and sitegen for complex bounded operators
16. new entry: Complex_Bounded_Operators
17. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains
18. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07;
19. clarified timeout; tuned whitespace;
20. hide_lams ~> opaque_lifting;
21. clarified antiquotations;
22. proper inst table;
23. clarified antiquotations;
24. clarified antiquotations;
25. proper inst table;
26. clarified antiquotations;
27. clarified antiquotations;
28. clarified antiquotations;
29. clarified antiquotations;
30. unused;
31. merged
32. clarified antiquotations;
33. proper match against const_name;
34. tuned;
35. tuned;
36. clarified antiquotations;
37. clarified antiquotations;
38. clarified antiquotations;
39. fix(ci): clarified addresses, set proper TLS version;
40. feat(ci): remove hard-coded address;
41. feat(SpecCheck/Show) tune pretty printing for environments
42. merge
43. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib"
44. new entries by Mihails Milehins CZH_Elementary_Categories, CZH_Foundations, CZH_Universal_Constructions, Conditional_Simplification, Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension
45. New entry: Dominance_CHK
46. Schutz_Spacetime website
47. new entry Schutz_Spacetime
48. metadata for Logging_Independent_Anonymity
49. new entry Logging_Independent_Anonymity