Changes

Summary

1. merged
2. sitegen for Continued_Fractions
3. New entry "Continued_Fractions"
4. sitegen for Approximate_Model_Counting
5. tuned (removing warnings)
6. new entry Approximate_Model_Counting
7. Go: website updates
8. Go submission
9. adapt to Isabelle/11a1f4d7af51;
10. use emph instead of italic;
11. tuned;
12. clarified names;
13. tuned lemmas
14. merged
15. removed stuff moved to the Isabelle distribution
16. avoid java.net.URL, following Isabelle/a4118f530263;
17. updated: standard Borel
18. use time_fun command
19. merged
20. Splay tree analysis now uses time_fun command
21. tuned proofs to reduce verification time following Isabelle/7735645667f0
22. merge
23. feat(Transport) major improvement of overloaded properties + new relational properties
24. fix(ML_Unification) replace binders before aeconv (avoids lowering)
25. feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code
26. merged
27. adapted to new definition of wf following Isabelle/033f90dc441d
28. merged
29. Two new lemmas by Eberl (requested by Paulson)
30. adapted to isabelle/devel
31. adapted to new definition of wfP following Isabelle/233d70cad0cf
32. updated url
33. merged
34. tuned proof
35. Patching some proofs, for of_nat_int_ceiling
36. Deletion of material that had been moved to the distribution
37. Multirelations_Heterogeneous: further results for convex-closure
38. added some material about the Laurent expansion of zeta
39. Remove stuff following Isabelle/d0205dde00bb and related changesets
40. fixed broken definitions and proofs following Isabelle/8d153846f65f
41. Universal_Hash_Families: Remove accidental duplication of pmf_of_set_prod_eq.
42. Inserted a corollary to the main result
43. Updated a proof to the new formalisation of meromorphic
44. Relational_Cardinality: minor revision
45. adapted to Isabelle/2746dfc9ceae;
46. merge
47. adjusting HOL-CSP_OpSem from 2023 to devel
48. merge from AFP 2023
49. metadata for HOL-CSP OpSem and sitegen
50. new entry: HOL-CSP OpSem
51. removed lemmas following Isabelle/ba8fb71587ae
52. merge from AFP 2023
53. sitegen for Wieferich Kempner
54. new entry: Wieferich Kempner
55. merge from AFP 2023
56. metadata and sitegen for QBF-Solver
57. new entry: QBF_Solver_Verification
58. further files for CubicalCategories
59. New entry CubicalCategories
60. update doc;
61. Correction of an error in the abstract
62. sitegen for Karatsuba
63. New submission: Karatsuba
64. adjusted proof
65. more accurate timeout; tuned whitespace;
66. move multiset lemmas into distro
67. non-executable files;
68. Moving library material into Analysis (Elementary_Metric_Spaces and Set_Integration)
69. New version consistent with paper
70. tuned proof: avoid z3 to make it work on arm64-linux;
71. tuned proof: avoid z3 to make it work on arm64-linux;
72. tuned proof: avoid z3 to make it work on arm64-linux;
73. tuned proof: avoid z3 to make it work on arm64-linux;
74. tuned whitespace;
75. tuned proof: avoid z3 to make it work on arm64-linux;
76. tuned whitespace;
77. backed out changeset ddf90847bfa5: still requires approx. 8-10h elapsed time / 50h CPU time on common test hardware (see 13b3e24a71b0), only latest x86_64-linux hardware is reasonably fast (3.5h elapsed time, 20h CPU time seen on of1.proof.cit.tum.de), but arm64-darwin is very slow;
78. tuned signature, following Isabelle/da4e82434985;
79. adapted to Isabelle/3648e9c88d0c;
80. Fixed a rewriting issue
81. Resolved a syntax clash involving Equipollence (now imported by Ramsey)
82. enable proof in session Lorenz_C1
83. simplified proofs
84. simplified proof
85. Incorporating library material from AFP sessions
86. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic
87. merged
88. Removed numerous z3 calls and tried to simplify some extremely messy proofs
89. Adjustments for recent changes to the main repository
90. A little tidying up. Removed some smt calls
91. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic
92. tuned proofs
93. Simpl: remove stray thm command
94. CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218fa
95. Interval_Analysis: adapt to isabelle@cff4576218fa
96. merge from afp-2023
97. update Simpl entry; change license to BSD (submission by Norbert Schirmer)
98. sitegen for IMP_Noninterference
99. New entry IMP_Noninterference
100. sitegen for Sumcheck Protocol
101. new entry Sumcheck Protocol
102. New entry OmegaCatoidsQuantales
103. New submission Region_Quadtrees
104. sitegen and metadata for Isabelle_hoops
105. New entry Isabelle_hoops (with its name standardised)
106. sitegen and metadata for Interval_Analysis
107. New submission Interval_Analysis
108. New entry CRYSTALS-Kyber_Security
109. proper Homepage comparison: URL equals does not fulfil specification;
110. A lot of tidying
111. merged
112. Tidied up some messy proofs
113. Cleaning and simplifying notation
114. A little tidying. Removal of z3 smt calls
115. formally normalized definition of singleton shifts to their primitive form
116. Integration syntax
117. Importation of the infinite type class
118. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
119. Moving a few facts from libraries into the main repository
120. Shortening some proofs
121. Correcting misleading notation
122. simplified class specification
123. more realistic timeouts;
124. Borrowed prod_mono_strict' for the distribution; adjusted proofs
125. merged
126. added lifting of forward simulation to transitive closure
127. Renamed a theorem involving convexity
128. Updated a proof for the corrected version of convex_on
129. Made the proof slightly more explicit
130. Fixed a problem involving sum_diff_split
131. New lemmas and renaming of lemmas
132. feat(ML_Unification,Transport) more robust unification + new unifiers
133. strengthened class parity
134. "Moving up" AFP library material to more appropriate places
135. merged
136. Simplification of some of the lemma libraries
137. merged
138. use define_time_function
139. common type class for trivial properties on div/mod
140. Expander_Graphs: Add additional tail bound for expander random walks.
141. rearranged and reformulated abstract classes for bit structures and operations
142. Universal_Hash_Families and Expander_Graphs: Framework for pseudorandom objects Pseudorandom objects as a combinator library was formerly incorrectly part of the Distribtued_Distinct_Elements AFP entry due to chronological reasons. But it belongs conceptually to the Universal_Hash_Families and Expander_Graphs entries, which this patch accomplishes. Compared to the former development in DDE the new framework also includes several improvements: - Constructive implementation of hash families - An object is always non-empty - this means every object induces naturally a PMF, which removes a lot of constraints from the theorems. Note: The theory DDE/Pseudorandom_Combinators is now obsolete. I will remove it shortly before the next release (to minimize the possibility of merge-conflicts).
143. tuned signature;
144. adapted to Isabelle/c7a98469c0e7;
145. Frequency_Moments and Expander_Graphs: Change the dependency between the entries. The dependency of Expander_Graphs to Frequency_Moments was due to the use of some auxiliary results (in particular those about HOL-Probability.Product_PMF). This change moves those to Universal_Hash_Families, so that the dependency can be avoided. Note: I added aliases and abbreviations to minimize the risk of merge-conflicts. This change will enable the introduction of further additional examples, that show how Expander Graphs can be used to further improve the space complexity of the verified algorithms in Frequency_Moments.
146. merge
147. feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations
148. Universal_Hash_Families: Remove duplicate proofs (caused by previous commit.)
149. Finite_Fields: Add exectuable algorithms for the construction of (and calculation in) finite fields.
150. Finite Fields: Minor improvements to previous commit.
151. Finite_Fields: Add Rabin's test for the irreducibility of polynomials.
152. Finite Fields: Add more general lower estimate for cardinality of irreducible polynomials.
153. Distributed_Distinct_Elements: Add related entries.
154. Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities.
155. Renamed a theorem
156. streamlined type class specification
157. consolidated lemma name
158. simplified specification of type class
159. consolidated name of lemma analogously to nat/int/word_bit_induct
160. tuned finite proofs
161. merged
162. adapted to Isabelle/7d10708bbc32;
163. adapted to isabelle/devel
164. Relational_Disjoint_Set_Forests: minor revision
165. more realistic timeout;
166. fix(ML_Unification) use cartouches to fix document build error
167. feat(ML_Unification) more explanation
168. merge
169. feat(Transport) better relativised concept definitions and lemmas
170. feat(ML_Unification) add recursive unification hints fallback option
171. CZH_Foundations: integration with Cardinality_Continuum
172. tuned;
173. tuned;
174. adapted to Isabelle/e1895596e1b9;
175. adapted to Isabelle/c6c2e41cac1c;
176. proper terminology;
177. removed outdated comments;
178. adapted to Isabelle/70c0dbfacf0b;
179. tuned;
180. tuned, following Isabelle/8c9cce335a3d;
181. tuned;
182. tuned;
183. tuned;
184. tuned;
185. tuned;
186. tuned, following Isabelle/e7796c55d840;
187. Hello_World: add some descriptive text
188. Introduced definition for the sigma algebra at infinity for a filtration.
189. Fixed issue that caused Martingales to not compile. Sorry!
190. re-introduce code in session of Hello_World
191. adapted to Isabelle/032a31db4c6f;
192. adjusted HOL-CSPM from 2023 to development (Patch.thy might need further cleanup)
193. Updated entry Martingales.
194. adapted Disintegration to devel
195. adapted to isabelle-dev;
196. adjusted Concentration Inequalities from 2023 to devel
197. merge from AFP 2023
198. tuned
199. New entry KnuthMorrisPratt
200. metadata and sitegen
201. new entry: HOL-CSPM
202. sitegen for Martingales
203. new entry Martingales
204. sitegen for Concentration_Inequalities
205. new entry Concentration_Inequalities
206. New entry: Lambert_Series
207. adjusted doi capitalization
208. sitegen for Q0_soundness
209. new entry Q0_Soundness
210. sitegen for Cardinality_Continuum
211. new entry Cardinality_Continuum
212. Polylog web files
213. sitegen for Polylog
214. New entry: Polylog
215. sitegen for Polynomial_Crit_Geometry
216. new entry Polynomial_Crit_Geometry
217. sitegen for Chebyshev_Polynomials
218. New entry Chebyshev_Polynomials
219. more website for LTL and PD
220. website for LTL and PD
221. Labeled_Transition_Systems and Pushdown_Systems
222. New entry: Nominal_Myhill_Nerode
223. more doc;
224. sitegen for Q0_Metatheory
225. updated LaTeX citations
226. new entry Q0_Metatheory
227. Perfect_Fields and Elimination_Of_Repeated_Factors incl sitegen
228. New entry Perfect_Fields
229. sitegen for /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Disintegration
230. New entry "Disintegration"
231. allow partially detecting potential name conflicts;
232. added check to detect potential name conflicts;
233. add warning for missing DOI cache;
234. Eudoxus_Reals patch and sitegen
235. New entry, Eudoxus_Reals
236. New entry /Hypergraph_Colourings
237. adapted to Isabelle/99bc2dd45111;
238. adapted to simplified T convention
239. merged
240. adapted to new T conventions
241. extracted lemma finite_progress out of proof
242. simplified proof
243. merged
244. tuned lift_strong_simulation_to_bisimulation
245. simplified definition of match_bisim
246. strengthened lift_strong_simulation_to_bisimulation and simplified match_bisim
247. adadpted to [simp] changes in distrib
248. de-duplicated specification of class ring_bit_operations
249. adjusted T_sift_down: all primitives take 0 time.
250. added missing file following 2702f2046afa
251. documented change in VeriComp
252. added framework-independent lemma to lift simulation to bisimulation
253. tuned
254. added publication
255. slightly more elementary characterization of unset_bit
256. base abstract specification of NOT on recursive equation rather than bit projection
257. more realistic timeouts for lrzcloud2:threads=1;
258. tuned proof
259. more realistic timeouts for lrzcloud2:threads=1;
260. operations AND, OR, XOR are specified by characteristic recursive equation
261. some extensions to Cotangent_PFD_Formula
262. slightly less technical formulation of very specific type class