Changes

Summary

1. modify JinjaDCI
2. Merged.
3. Various tuning that for some reason didn't get merged from my master branch.
4. A spot of polishing
5. Merged.
6. Update metadata to reflect changes made in July, 2021.
7. Add a revision note concerning material added in July, 2021.
8. tuned signature, according to Isabelle/042041c0ebeb;
9. Merged.
10. Sync with my development repo.
11. Adjust Imperative List/Map/Set Specification for more lenient next operation This allows implementations of this iterator specification to make use of temporary variables for obtaining the next element of the list/set/map. This is required by some and especially more general iterators.
12. discontinued obsolete "val extend = I" for data slots;
13. tuned;
14. merged
15. metadata update for MFODL_Monitor_Optimized
16. fixed a mistake in MFODL_Monitor_Optimized
17. merge
18. adjusted Virtual-Substitution from 2021 to devel
19. merge of AFP 2021
20. fixed duplicate "and"
21. sitegen for Virtual_Substitution
22. new entry: Virtual Substitution
23. updated website/email address
24. modify JinjaDCI
25. modifications in Jinja and DOminance_CHK
26. modifications in Jinja and Dominance_CHK
27. merged
28. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f);
29. more accurate treatment of context;
30. more accurate treatment of context;
31. more accurate treatment of context;
32. tuned -- proper names/scopes for contexts;
33. tuned proofs;
34. more accurate treatment of context;
35. more accurate treatment of context;
36. proper antiquotations;
37. tuned messages;
38. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts; tuned whitespace;
39. dead code!?
40. clarified signature, following Isabelle/de4f151c2a34;
41. modifications in Jinja and Dominance_CHK
42. CZH: large limits, generalizations, a variety of minor amendments
43. Simplified a definition
44. modify propa
45. bit singleton shifts recovered for the sake of backward compatibility
46. updated to 7422950f3955
47. merge
48. EPO: simplify proof
49. primer
50. more complete simp rules
51. more complete simp rules (examples)
52. avoid overaggressive contraction of conversions
53. slightly more prominence for proof tools; more examples
54. ETTS: minor amendments
55. CTR and ETTS: integration with fd5f62176987
56. adapted QHLProver to isabelle-dev/409ca22dee4c
57. adapted to isabelle-dev/409ca22dee4c
58. adapted to devel
59. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5
60. Weighted_Path_Order: update to isabelle@ffb15f7f26d5
61. merge from afp-2021
62. add missing session dependency
63. new entry FOL_Axiomatic
64. regen website
65. minor editorial changes for CZH entries
66. New entry Weighted_Path_Order
67. fxed metadata (forgot .html) in link
68. metadata and sitegen for complex bounded operators
69. new entry: Complex_Bounded_Operators
70. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains
71. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07;
72. clarified timeout; tuned whitespace;
73. hide_lams ~> opaque_lifting;
74. clarified antiquotations;
75. proper inst table;
76. clarified antiquotations;
77. clarified antiquotations;
78. proper inst table;
79. clarified antiquotations;
80. clarified antiquotations;
81. clarified antiquotations;
82. clarified antiquotations;
83. unused;
84. merged
85. clarified antiquotations;
86. proper match against const_name;
87. tuned;
88. tuned;
89. clarified antiquotations;
90. clarified antiquotations;
91. clarified antiquotations;
92. fix(ci): clarified addresses, set proper TLS version;
93. feat(ci): remove hard-coded address;
94. feat(SpecCheck/Show) tune pretty printing for environments
95. merge
96. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib"
97. new entries by Mihails Milehins CZH_Elementary_Categories, CZH_Foundations, CZH_Universal_Constructions, Conditional_Simplification, Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension
98. New entry: Dominance_CHK
99. Schutz_Spacetime website
100. new entry Schutz_Spacetime
101. metadata for Logging_Independent_Anonymity
102. new entry Logging_Independent_Anonymity
103. repaired slip
104. feat(SpecCheck) folder renaming, types for tests
105. tuned
106. mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f;
107. ported Design-Theory from AFP 2021 to devel
108. ported Three-Circles from AFP 2021 to devel
109. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers
110. ported Cubic_Quartic_Equations from AFP 2021 to devel
111. merge of AFP 2021
112. Cubic_Quartic_Equations sitegen
113. new entry Cubic_Quartic_Equations
114. sitegen for combinatorial design theory
115. new entry: Combinatorial Design Theory
116. sitegen for Three Circles
117. new entry: Three Circles
118. clarified modules, according to Isabelle/534b231ce041;
119. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15; subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65);
120. clarified signature, according to Isabelle/d882abae3379;
121. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
122. tuned signature, according to Isabelle/28a582aa25dd;
123. eliminated Specification.definition', following Isabelle/6876e3d5e362;
124. clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a;
125. clarified signature, according to Isabelle/612b7e0d6721;
126. tuned signature, according to Isabelle/839a6e284545;
127. merged
128. Backed out changeset ef19e4e58b8c restoring old argument order on synthesized formulas
129. avoid hardwired document;
130. merged
131. tuned signature, according to Isabelle/9d9e7ed01dbb;
132. clarified signature, according to Isabelle/9d9e7ed01dbb;
133. clarified signature, according to Isabelle/9d9e7ed01dbb;
134. clarified signature, according to Isabelle/9d9e7ed01dbb;
135. simplified, using Isabelle/ML operations;
136. adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars;
137. tuned whitespace;
138. more scalable operations;
139. merged
140. synthesized formulas have their variables permuted
141. merged
142. fixes for cardinality lemmas
143. proper inst table;
144. Graphic rendering of Relational_Method PDF files refined.
145. Entry Relational_Method updated.
146. more realistic timeout;
147. clarified signature;
148. follow Isabelle/53e28c438f96;
149. clarified signature, following Isabelle/a3b0fc510705;
150. merged
151. tuned
152. consolidation of rules for bit operations
153. tuned name
154. Fix typo
155. Tune references ... using new name of BD_Security_Compositional
156. Remove redundant license
157. more realistic timeout: approx. 5min CPU time;
158. cleaning up
159. New entry CoSMeDis
160. New entry CoSMed
161. New entry: BD_Security_Compositional
162. New entry: CoCon
163. updated to devel
164. merge from AFP 2021
165. New entry Fresh_Identifiers
166. New entry: Relational_Forests
167. cleaning up
168. merged
169. cleaning up
170. Update Bounded_Deducibility_Security - Generalise BD Security from I/O automata to nondeterministic transition systems, with the former retained as an instance of the latter (renaming locale BD_Security to BD_Security_IO) - Generalise unwinding conditions to allow making more than one transition at a time when constructing alternative traces, giving more flexibility for unwinding strategies - Add various helper lemmas and definitions - Add results about the expressivity of declassification triggers vs. bounds, due to Thomas Bauereiss (added as author)
171. tuned signature, following Isabelle/069f6b2c5a07;
172. metadata update for MFMC_Countable
173. derive rel_pmf characterization from bounded and unbounded MFMC theorem
174. merged
175. drop boundedness requirement for the sink
176. avoid global tmp file: pointless due to implicit theory export;
177. repaired syntax
178. tuned signature, following Isabelle/d030b988d470;
179. generalized gt_rat_sign_change to square-free polynomials
180. minor updates to bibliography
181. clarified signature;
182. clarified abstract and concrete boolean algebras
183. antiquotation for bundles
184. simplified hierarchy of type classes for bit operations
185. restored executable conversions
186. dropped junk
187. moved theory Bit_Operations into Main corpus
188. organize syntax for word operations in bundles
189. more systematic approach for instantiation
190. avoid seemingly unused transfer rules
191. cleaner presentation of analysis theorems in preliminaries
192. Update to new Epistemic_Logic.thy
193. Avoid typedefs
194. Clean: set AFP standard document options
195. Clean: re-add to chapter AFP
196. merge from afp-2021
197. Finitely_Generated_Abelian_Groups website
198. new entry Finitely_Generated_Abelian_Groups
199. Added Finitely_Generated_Abelian_Groups to metadata
200. Sync with my development repo. Add new material: "concrete bicategories" and "bicategory of categories". Change sublocale declarations related to functor/natural transformation/natural isomorphism to avoid issues with global interpretations reported by Filip Smola, 2/2/2021.
201. compile
202. more realistic timeout: 50min CPU time;
203. Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending on Finitely_Generated_Abelian_Groups
204. new entry Finitely_Generated_Abelian_Groups
205. remove duplicate entry in metadata
206. more coherent dependencies
207. fix(Regex_Equivalence) update to new SpecCheck version
208. operations for symbolic computation of bit operations
209. fixed Proof_Strategy_Language following Isabelle/f58108b7a60c
210. SpecCheck now without _ (Regex_Equivalence is still broken)
211. T1 fontenc for new entries
212. sitegen
213. update hide_lams -> opaque_lifting
214. merged from afp2021
215. website for SpecCheck
216. new entry SpecCheck
217. metadata and sitegen for MiniSail
218. new entry: MiniSail
219. sitegen for Public Announcement Logic
220. new entry "Public Announcement Logic" (and sorted ROOTS + removed duplicate entries in ROOTS)
221. fixed a messy reference
222. Van_der_Waerden website
223. new entry Van_der_Waerden
224. New entry IMP_Compiler
225. Removal of unintended files
226. Hidden.thy to Isar
227. merged
228. renamed hide_lams opaque_lifting
229. merged
230. changed to opaque_lifiting as suggested by Isabelle/Jenkins
231. changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins