Changes

Summary

1. fix dangerous context management
2. A slightly stronger lemma allowing slightly simpler proofs
3. Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself
4. Elimination of all z3 calls
5. Word_Lib sync from l4v; tweak word_eqI
6. generalise word_eqI method; make sure it is exercised
7. test_bit_size not longer needed; avoid potential nontermination
8. Word_Lib tweaks for slightly more backwards compatibility
9. use bit_simps in word_eqI method
10. adapted to new version of Infinite_Sum in isabelle-dev
11. avoid hardwired document output;
12. CTR and ETTS: integration with SpecCheck: minor amendments
13. Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum
14. Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum
15. merge
16. merge
17. Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc.
18. documentation fine-tuning.
19. Added section on C11_Ast_Lib in chapter II.
20. Example section restored and Documentation adapted.
21. Stramge intermediate configuration: Example section zerschossen.
22. Port to Isabelle2021-1 RC 2.
23. Improved documentation.
24. Examples for iterator - applications: queries, and translations into term.
25. Rearranging standard root store; better documentation in C_Command.
26. Rearranging the ML _programming Example Section C1.
27. reorg 1
28. ...
29. Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy)
30. Restructuring of Interfaces; more show cases.
31. Updated meta-data for Optics
32. Additional scene laws
33. Branch merge
34. Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables.
35. feat(SpecCheck/Show) add parentheses for option SOME case
36. merged
37. weakened ordering requirements
38. used well-founded pre-order in standard redundancy criterions
39. derived refutational completeness from finitary and non-finitary standard redundancy criterion
40. merge
41. deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since they are now available as complete methods in Factor-Algebraic-Polynomial
42. factor_complex_poly delivers distinct list
43. merged
44. Removal of material that's going to be in Isabelle2021-1
45. merge
46. refactoring (moving theories and lemmas around)
47. sync from l4v
48. adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3)
49. merge of afp-2021
50. new entry PAL
51. new entry Factor_Algebraic_Polynomial
52. merge from afp-2021
53. document `publish -`
54. changed affiliation of eberl (this time properly)
55. changed affiliation of Eberl
56. sitegen for Real_Power
57. new entry Real_Power
58. New entry Szemeredi_Regularity
59. tuned proofs -- avoid z3;
60. CTR and ETTS: integration with SpecCheck
61. used antiquotation to fix LaTeX failure
62. adapted to devel
63. updated to devel
64. merged
65. tuned proof for devel
66. clarified quotes vs. apostrophes vs. primes;
67. more accurate use of LaTeX ndash;
68. prefer portable LaTeX mdash;
69. tuned whitespace --- removed suspicious Unicode;
70. proper Unix linefeeds;
71. changed affiliation of eberl (this time properly)
72. changed affiliation of eberl
73. added author to Saturation_Framework_Extensions
74. derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy
75. added locale calculus_with_finitary_standard_redundancy
76. 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.)
77. feat(SpecCheck) add better unit tests facilities, examples and exceptions property
78. discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author);
79. Correctness_Algebras: increase nitpick timeout
80. CZH: dagger monoidal categories
81. update it Isabelle/925b46043b84
82. merge from afp-2021
83. sitegen for Registers
84. new entry Registers
85. Correctness_Algebras: increase session timeout
86. tuned signature, according to Isabelle/df12779c3ce8;
87. feat(SpecCheck) add possibility to make builds fail on failure and extend README
88. added missing funding information
89. restored theory structure for simple genericity.
90. Backed out changeset af549be0a8cd
91. restored different entrance points a before Isabelle2021
92. proper parentheses (amending 354560d7143a);
93. Adjusted to prospective release Isabelle2021-2.
94. Correctness_Algebras: uncomment counterexamples
95. clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead;
96. clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead;
97. merge from afp-2021
98. remove unused functions
99. silence sitegen warning
100. new entry X86_Semantics
101. adjust to isabelle@549019b4a808
102. merge from afp-2021
103. metadata for Belief_Revision
104. new entry Belief_Revision
105. New entry Correctness_Algebras
106. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;
107. updated metadata for Count_Complex_Roots
108. corrected the timeout for CZH_Universal_Constructions
109. CZH: further results about comma categories and Kan extensions, a variety of other minor amendments
110. more generic bit/word lemmas for distribution
111. Fixing a name clash between two different "restrict" operators
112. Merged
113. solved the roots-on-the-border problem
114. split Count_Complex_Roots
115. more realistic timeout;
116. clarified signature, according to Isabelle/ccf599864beb;
117. back to dedicated separate shift operations for infix syntax; more default simp rules on closed numeric expressions