Build #71 (Sep 26, 2021, 12:14:00 AM)

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

1. ported Design-Theory from AFP 2021 to devel (detail)
2. ported Three-Circles from AFP 2021 to devel (detail)
3. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers (detail)
4. ported Cubic_Quartic_Equations from AFP 2021 to devel (detail)
5. merge of AFP 2021 (detail)
6. Cubic_Quartic_Equations sitegen (detail)
7. new entry Cubic_Quartic_Equations (detail)
8. sitegen for combinatorial design theory (detail)
9. new entry: Combinatorial Design Theory (detail)
10. sitegen for Three Circles (detail)
11. new entry: Three Circles (detail)
12. clarified modules, according to Isabelle/534b231ce041; (detail)
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); (detail)
14. clarified signature, according to Isabelle/d882abae3379; (detail)

Started by timer

This run spent:

• 28 ms waiting;
• 15 hr build duration;
• 15 hr total from scheduled to completion.