Changes

Summary

1. provide component naproche-2d99afe5c349;
2. merged
3. Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
4. more documentation about Type/Const antiquotations;
5. more documentation about document build options;
6. address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
7. tuned --- fewer IDE warnings;
8. more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;
9. added definitions multp{DM,HO} and corresponding lemmas
10. added wfP_less to wellorder and wfP_less_multiset
11. restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
12. merged
13. added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
14. redefined less_multiset to be based on multp
15. added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
16. added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
17. added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
18. added lemma wfP_multp
19. added lemma mono_multp
20. added Multiset.multp as predicate equivalent of Multiset.mult
21. address problems with launch4j and jdk-17 (see also 41d009462d3c);
22. more robust build on midrange hardware;
23. clarified tests: omit somewhat pointless (unstable) results;
24. proper fields for gnuplot (amending b614e3e4146a);
25. tuned output;
26. tuned;
27. merged
28. more robust build on midrange hardware (despite 67d6f1708ea4);
29. Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
30. updated to polyml-5.9;
31. NEWS on "isabelle mirabelle";
32. tuned;
33. clarified default for kodkod_scala; NEWS for proper release;
34. maintain option kodkod_scala within theory context, to allow local modification;
35. NEWS for proper release;
36. updated to flatlaf-1.6.4;
37. avoid broken links: auxiliary files are not yet supported;
38. option document_comment_latex supports e.g. Dagstuhl LIPIcs;
39. more explicit type Latex.Tags; generate isabelletags.sty from Isabelle/Scala, including comment.sty setup;
40. more uniform treatment of optional_argument for Latex elements; discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML; clarified signature of class Latex: overridable unknown_elem allows to extend the markup language;
41. removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
42. example: alternative document headings, based on more general document output markup;
43. more general document output: enclosing markup is defined in user-space;
44. clarified modules (see c299abcf7081);
45. output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
46. clarified modules;
47. tuned signature: more explicit types for presentation;
48. more robust support for Windows line-endings;
49. source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;
50. more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;
51. clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
52. more symbolic latex_output via XML (using YXML within text);
53. proper enclose_name (amending e77c5bfca9aa);
54. Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;
55. more symbolic latex_output via XML;
56. clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
57. tuned;
58. tuned;
59. updated to verit-2021.06.2-rmx;
60. clarified HTML_Context.theory_exports: prefer value-oriented parallelism;
61. generate problems with correct logic for veriT
62. more parallelism, at the cost of potential duplicates of make_thy;
63. afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);
64. more interrupts;
65. present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826; eliminated implicit state: these theories are globally unique;
66. tuned;
67. clarified modules;
68. tuned (see also e0d1d9203275);
69. clarified signature;
70. tuned;
71. spelling;

Summary

1. feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times
2. Tuned: use a star in witness.
3. merge from afp-2021-1
4. adjust for new tags in Isabelle2021-1-RC4
5. fix dangerous context management
6. In the definition of regular pair, switched from strict to non-strict
7. Rename H to S in maximal_exactly_one.
8. Get rid of the sat abbreviation.
9. Add missing spaces in semantics_tm.
10. No space in front of object-logic forall.
11. Non-conflicting name for boolean denotation.
12. Simpler Hintikka definition.
13. Add syntactic abbreviation for constants.
14. fixed lemma following Isabelle/c256bba593f3
15. fix dangerous context management