Changes

Summary

1. proper use of antiquotations;
2. more documentation on "Conversions";
3. tuned
4. updated example;
5. clarified options (again);
6. more options: update ISABELLE_IDENTIFIER;
7. clarified conditional ML;
8. support for conditional ML text;
9. updated example;
10. clarified options;
11. proper context variable handling when stripping leadings quantifiers from test goals
12. proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);
13. eliminated perl: prefer elementary GNU printenv;
14. more robust bootstrap of components;
15. more self-contained support for macOS;
16. misc tuning and clarification;
17. tuned signature;
18. support for base64 via Isabelle/Scala/ML;
19. compile;
20. clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
21. clarified signature (again);
22. merged
23. clarified signature;
24. unused;
25. unused;
26. clarified signature: more structured arguments, notably for remote provers;
27. clarified signature;
28. clarified signature: avoid tmp file;
29. clarified signature for Scala functions;
30. clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);
31. tuned;
32. clarified cache;
33. clarified signature: Bytes extends CharSequence already (see d201996f72a8);
34. clarified exceptions;
35. more uniform use of Byte_Message; support protocol_message with multiple chunks;
36. tuned signature;
37. tuned signature;
38. more robust treatment of empty markup: it allows to produce formal chunks;
39. collected combinatorial material
40. tuned;
41. tuned;
42. more documentation;
43. proper treatment of nested antiquotations; clarified signature;
44. support for ML special forms: modified evaluation similar to Scheme;
45. clarified signature: more detailed token positions for antiquotations;
46. merged
47. clarified signature;
48. confluent preprocessing for floats in presence of target language numerals
49. subclass relation
50. some tinkering with npm versions;
51. some tinkering with npm versions;
52. back to post-release mode;
53. tuned signature;
54. auto-update due to "isabelle build_vscode";
55. tuned;
56. tuned --- following hints by IntelliJ IDEA;
57. fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)
58. simplified definition
59. new lemmas
60. discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";
61. following recent Phabricator update, after 2021 Week 13 (Late March);
62. merged
63. Cosmetic: no !! in the lemma statement
64. clarified README; avoid odd patching of sources;
65. more standard header, with utf-8 encoding;
66. clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
67. merged
68. new automatic order prover: stateless, complete, verified
69. clarified signature;
70. clarified: follow "isabelle version -t";
71. further clarification of Isabelle distribution identification -- avoid odd patching of sources;
72. tuned signature -- more explicit types;
73. more robust and uniform ISABELLE_TAGS;
74. clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
75. simplified release status (again), in contrast to a43898f76ae9;
76. more uniform HTTP resources;
77. clarified (again): local tip could be actually more recent;
78. tuned;
79. tuned;
80. clarified name;
81. more systematic java_library: avoid empty entries, declaration order as for other bash functions;
82. support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
83. updated to latest latex due to new mechanism for dealing with bold ccfonts
84. removal of needless hypothesis in hd_rev and last_rev

Summary

1. more realistic timeout;
2. tuned whitespace;
3. Tweaks
4. adapted to Isabelle/a2c589d5e1e4;
5. Merge
6. tweak
7. simplified proof
8. sshiftr/bl lemmas by Florian Märkl
9. proof simplification
10. cosmetic tweaks to proofs
11. merged
12. minor stylistic changes
13. Add completeness of modal logics T, KB, K4, S4 and S5
14. Stylistic tweaks, which I hope are improvements :-)
15. updated paper references
16. merge
17. increased timeout
18. collected combinatorial material
19. Update root.tex
20. Cut out Fitting's consistency properties
21. fixed proof
22. clarified message, following Isabelle/a7aabdf889b7;
23. confluent preprocessing for floats in presence of target language numerals
24. subclass relation
25. adapted to isabelle-dev/56db8559eadb
26. simplified definition
27. new lemmas
28. probable fix suggested by Cornelius for the changes in the vicinity of 2cd23d587db9
29. Fixes due to new order prover
30. another broken proof
31. Fixed and simplified some failing proofs
32. Writing less_sets as an infix
33. avoid symblinks --- make it work on Windows;
34. Fixed some looping proofs (though why they were looping isn't clear)
35. Fixed a failing proof
36. merged
37. fixes for new hd_rev and last_rev