Changes

Summary

1. merged
2. some new and/or varient results about images
3. nicer statement of Liouville_theorem
4. more lemmas
5. max word moved to Word_Lib in AFP
6. more robust syntax;
7. unused;
8. clarified document export names;
9. tuned signature;
10. tuned;
11. tuned;
12. avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
13. compose Latex text as XML, output exported YXML in Isabelle/Scala;
14. more direct index_entry: no positions required -- text is eventually moved to .ind file;
15. clarified signature;
16. clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
17. tuned message, e.g. for Pure bootstrap;
18. proper signature export (amending b50f8cc8c08e);
19. syslog option for "isabelle build";
20. further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);
21. merged
22. NEWS;
23. clarified index, more like formal @{element_ref};
24. clarified treatment of type constructors;
25. misc tuning and clarification;
26. tuned signature;
27. clarified context;
28. more uniform document antiquotations for ML: consolidate former setup for manuals;
29. clarified names;
30. clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
31. clarified modules;
32. clarified modules;
33. tuned;
34. clarified signature: avoid dispatch via name;
35. clarified, e.g. type variables;
36. tuned index;
37. more ambitious default for index "is like";
38. tuned;
39. support for index entries;
40. tuned;
41. tuned signature;
42. clarified modules;
43. clarified old document build;
44. unused;
45. prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee;
46. prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document;
47. unused;
48. proper Unix lines;
49. prefer explicit option document_bibliography (actually ignored by build script);
50. explicit option document_bibliography;
51. proper bibliography;
52. discontinued obsolete "isabelle latex";
53. more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; clarified ISABELLE_MAKEINDEX options;
54. default document_build (lualatex);
55. more robust: allow \printindex within the document;
56. clarified bash scripts, with public interfaces for user-defined Document_Build.Engine;
57. tuned signature;
58. option document_preprocessor;
59. show symbols in Isabelle/ML instead of perl;
60. more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;
61. tuned --- more robust;
62. discontinued somewhat pointless "fixbookmarks": default output works sufficiently well;
63. more uniform bibtex error, without using perl (see 4710dd5093a3);
64. proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);
65. tuned;
66. clarified command-line options;
67. obsolete (see 5a3a2a52648d);
68. redundant: copy produced from session document_files;
69. clarified treatment of Isabelle .sty files;
70. option document_logo;
71. proper options;
72. option document_build refers to build engine in Isabelle/Scala; pdflatex is back as legacy build engine, e.g. for published proceedings;
73. redundant: tmp_dir is purged anyway;
74. misc tuning and clarification;
75. clarified modules;
76. tuned --- clarified corner cases;
77. more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;
78. clarified signature -- avoid odd warning about scala/bug#6675;
79. tuned;
80. tuned;
81. clarified signature;
82. proper syntax of Scala 3;
83. enforce syntax of Scala 3;

Summary

1. complement reduced to mere abbreviation
2. extracted more legacy abbreviations
3. max word moved to Word_Lib in AFP
4. merge from afp-2021
5. update website
6. fix links
7. Restore deleted theorem from Szpilrajn
8. tuned presentation
9. adapted to devel
10. adjusted to changes in distribution
11. adjust Combinatorics_Words to isabelle@493b1ae188da
12. merge from afp-2021
13. make AFP ROOTS globally available for component
14. merged
15. New entries Combinatorics_Words*
16. adjusted to change in distribution
17. adapted to Isabelle/466fae6bf22e;
18. tuned whitespace;
19. Remove comment about missing refinement
20. continued uglification, but also fixed some dodgy proofs
21. fixed some broken / looping / fragile proofs
22. merge from afp-2021
23. simplify usage instructions more
24. sitegen for Padic_Ints
25. new entry: Padic_Ints
26. update affiliation
27. New entry: Regressioon_Test_Selection
28. metadata for Metalogic_ProofChecker
29. new entry Metalogic_ProofChecker
30. metadata for GaleStewart_Games
31. new entry GaleStewart_Games
32. fixed the ROOT file ofr BenOr_Kozen_Reif
33. webpage for BenOr_Kozen_Reif
34. new entry BenOr_Kozen_Reif
35. Slight tidying to shorten too-long lines
36. added a necessary acknowledgment (ERC)
37. New entry Progress_Tracking
38. Revisions by Wenda to eliminate the locale comp_affine_scheme
39. renamed a lemma
40. Fixed an error in the statement of closed_subsets_empty. Also added syntax priority hints for carrier_of_local_ring_at.
41. consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry + sitegen
42. new entry: Grothendieck_Schemes
43. metadata for IFC_Tracking
44. new entry IFC_Tracking
45. merged
46. adapted to Isabelle/ef1a18e20ace;
47. recover some patches after years of continuously changing Isabelle LaTeX output;
48. prefer document_preprocessor over document_build;
49. prefer document_logo instead of document_build script;
50. proper options;