Changes

Summary

1. merged
2. tuned (thanks to J. Villadsen)
3. added padding to Mirabelle's output
4. merged
5. tuned generation of TPTP with $ite/$let in higher-order logics
6. tuned generation of TPTP with $ite in function position
7. tuned TPTP generation of If helper facts
8. merged
9. clarified signature: prefer static operations;
10. clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
11. more robust;
12. tuned signature;
13. clarified signature: more explicit class Entity_Context with private state + operations;
14. more hyperlinks, notably internal fact references;
15. Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO
16. A tiny bit of tidying connected with Zorn's Lemma
17. tuned;
18. tuned;
19. proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
20. revert temporary workaround 6d111935299c;
21. added lemma
22. merged
23. tuned attributes to avoid looping
24. added eq_iff_swap for creating symmetric variants of thms; applied it in List.
25. tuned text;
26. more robust timeout, following df4449c6eff1;
27. more accurate Files.isRegularFile, exclude directories (e.g. jar_path);
28. proper java_version for isabelle_setup;
29. explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;
30. tuned;
31. repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process);
32. discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;
33. clarified messages, depending on option "document_echo";
34. just one cache, via HTML_Context, via Sessions.Store or Session;
35. merged
36. new lemmas about convex, concave functions, + tidying
37. proper support for arm64;
38. no perl (amending 59ef23ac81ab);
39. merged
40. Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b
41. merged
42. Preserve variable name z in VAR {z = t}
43. back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin;
44. updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default);
45. more precise URL
46. tuned page breaks

Summary

1. CTR and ETTS: integration with SpecCheck
2. used antiquotation to fix LaTeX failure
3. adapted to devel
4. updated to devel
5. merged
6. tuned proof for devel
7. clarified quotes vs. apostrophes vs. primes;
8. more accurate use of LaTeX ndash;
9. prefer portable LaTeX mdash;
10. tuned whitespace --- removed suspicious Unicode;
11. proper Unix linefeeds;
12. changed affiliation of eberl (this time properly)
13. changed affiliation of eberl
14. added author to Saturation_Framework_Extensions
15. derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy
16. added locale calculus_with_finitary_standard_redundancy
17. Registers: - Added mechanism for raising errors if autogenerated files need updating - Changed definition of Axioms_Quantum.register_pair (returns 0 for incompatible registers, see register_pair_is_register_converse for a useful consequence) - Slightly reducing namespace pollution in Classical_Extra (hiding consts x, y, X, Y etc.)
18. feat(SpecCheck) add better unit tests facilities, examples and exceptions property
19. discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author);
20. Correctness_Algebras: increase nitpick timeout
21. CZH: dagger monoidal categories
22. update it Isabelle/925b46043b84
23. merge from afp-2021
24. sitegen for Registers
25. new entry Registers