Changes

Summary

1. added lemmas
2. merged
3. tuned;
4. removed redundant test (see also 86fac52c2795, a9fea3f11cc0);
5. just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);
6. proper version;
7. back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);
8. less ambitious parallelism: more direct read/write saves overall heap space and GC time;
9. slightly faster XML output: avoid too much regrowing of StringBuilder;
10. updated NEWS: arm64-linux support is almost complete;
11. update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;
12. more material for HOL-Analysis.Infinite_Sum
13. more symbolic latex_output via XML;
14. clarified signature;
15. updated to polyml-5.9-610a153b941d -- close to final;
16. tuned signature (again): latex_output is likely to depend on context;
17. more symbolic latex output; discontinued Latex.output_text, which is in conflict with symbolic output;
18. tuned signature;
19. symbolic latex_output via XML, interpreted in Isabelle/Scala;
20. tuned signature;
21. clarified signature;
22. clarified signature;
23. clarified signature: more privacy;
24. tuned output --- less redundancy;
25. tuned whitespace;
26. clarified signature: Latex.Output as parameter to Document_Build.Engine; tuned;
27. proper detection of ARM platform variants;
28. back to post-release mode;
29. updated for release;
30. Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5
31. merged
32. updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default);
33. clarified HTML_Context: more explicit directory structure;
34. tuned comments;
35. tuned;
36. clarified signature;
37. clarified properties: avoid empty entry;
38. tuned signature;

Summary

1. A slightly stronger lemma allowing slightly simpler proofs
2. Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself
3. Elimination of all z3 calls
4. Word_Lib sync from l4v; tweak word_eqI
5. generalise word_eqI method; make sure it is exercised
6. test_bit_size not longer needed; avoid potential nontermination
7. Word_Lib tweaks for slightly more backwards compatibility
8. use bit_simps in word_eqI method
9. adapted to new version of Infinite_Sum in isabelle-dev
10. avoid hardwired document output;
11. CTR and ETTS: integration with SpecCheck: minor amendments
12. Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum
13. Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum
14. merge
15. merge
16. Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc.
17. documentation fine-tuning.
18. Added section on C11_Ast_Lib in chapter II.
19. Example section restored and Documentation adapted.
20. Stramge intermediate configuration: Example section zerschossen.
21. Port to Isabelle2021-1 RC 2.
22. Improved documentation.
23. Examples for iterator - applications: queries, and translations into term.
24. Rearranging standard root store; better documentation in C_Command.
25. Rearranging the ML _programming Example Section C1.
26. reorg 1
27. ...
28. Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy)
29. Restructuring of Interfaces; more show cases.
30. Updated meta-data for Optics
31. Additional scene laws
32. Branch merge
33. Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables.
34. feat(SpecCheck/Show) add parentheses for option SOME case
35. merged
36. weakened ordering requirements
37. used well-founded pre-order in standard redundancy criterions
38. derived refutational completeness from finitary and non-finitary standard redundancy criterion
39. merge
40. deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since they are now available as complete methods in Factor-Algebraic-Polynomial
41. factor_complex_poly delivers distinct list
42. merged
43. Removal of material that's going to be in Isabelle2021-1
44. merge
45. refactoring (moving theories and lemmas around)
46. sync from l4v
47. adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3)
48. merge of afp-2021
49. new entry PAL
50. new entry Factor_Algebraic_Polynomial
51. merge from afp-2021
52. document `publish -`
53. changed affiliation of eberl (this time properly)
54. changed affiliation of Eberl
55. sitegen for Real_Power
56. new entry Real_Power
57. New entry Szemeredi_Regularity
58. tuned proofs -- avoid z3;