Changes

Summary

1. merged
2. tuned proofs --- avoid 'guess';
3. apply declarations from interpretations in eigen context also
4. grant access to sun.tools.jconsole, as required for Java 17;
5. update to e-2.6, following Martin Desharnais;
6. updated to Metis 2.4 (release 20200713)
7. avoid problems with launch4j and jdk-17;
8. update to jdk-17+35 (LTS);
9. tuned message;
10. unused since 398b7bb9ebdd;
11. merged
12. removed checks for non-commercial usage of Vampire as it is now under BSD licence
13. enabled FOOL for Vampire in Sledgehammer
14. used Vampire 4.5.1 in Sledgehammer
15. proper NEWS;
16. tuned NEWS;
17. clarified antiquotations;
18. clarified antiquotations;
19. clarified antiquotations;
20. clarified partial application: immediate check of object-logic, and avoidance of context within closure;
21. merged
22. clarified antiquotations;
23. ML antiquotations for object-logic judgment;
24. proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
25. clarified modules;
26. clarified modules;
27. more uniform syntax;
28. permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
29. NEWS;
30. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
31. localized command 'syntax' and 'no_syntax';
32. tuned;
33. clarified signature;
34. clarified signature;
35. merged
36. proper constants in TPTP $let binding
37. more operations from Isabelle/ML;
38. merged
39. tuned proofs --- eliminated 'guess';
40. tuned proofs; tuned whitespace;
41. clarified antiquotations;
42. proper firstorderization in Sledgehammer
43. clarified signature; clarified antiquotations;
44. clarified antiquotations;
45. clarified signature -- prefer antiquotations (with subtle change of exception content);
46. more control symbols;
47. support ML antiquotations with fn abstraction;
48. unused;

Summary

1. ported Design-Theory from AFP 2021 to devel
2. ported Three-Circles from AFP 2021 to devel
3. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers
4. ported Cubic_Quartic_Equations from AFP 2021 to devel
5. merge of AFP 2021
6. Cubic_Quartic_Equations sitegen
7. new entry Cubic_Quartic_Equations
8. sitegen for combinatorial design theory
9. new entry: Combinatorial Design Theory
10. sitegen for Three Circles
11. new entry: Three Circles
12. clarified modules, according to Isabelle/534b231ce041;
13. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15; subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65);
14. clarified signature, according to Isabelle/d882abae3379;