#28 (Jul 13, 2023, 11:21:13 AM)

1. merge from afp-2022 (detail / hgweb)
2. re-generate site; (detail / hgweb)
3. tuned for smaller diffs; (detail / hgweb)
4. New topic for Gray_Codes (detail / hgweb)
5. More Gray_Codes (detail / hgweb)
6. More Gray_Codes (detail / hgweb)
7. New entry Gray_Codes (detail / hgweb)
8. metadata and sitegen for Executable_Randomized_Algorithms (detail / hgweb)
9. New entry Executable_Randomized_Algorithms (detail / hgweb)
10. new entry DCR-ExecutionEquivalence (detail / hgweb)
11. Zeckendorf: metadata and sitegen (detail / hgweb)
12. new entry Zeckendorf (detail / hgweb)
13. Crypto_Standards: Fixed a spelling error (detail / hgweb)
14. Crypto_Standards metadata & website (detail / hgweb)
15. New entry Crypto_Standards (detail / hgweb)
16. move TOML module to Isabelle (see Isabelle/be8aaaa4ac25); (detail / hgweb)
17. added missing timeout; (detail / hgweb)
18. reformat; (detail / hgweb)
19. remove duplicate fields; (detail / hgweb)
20. check TOML parse structure properly; (detail / hgweb)
21. proper typed TOML layer; (detail / hgweb)
22. tuned imports; (detail / hgweb)
23. Updated links (detail / hgweb)
24. Added citations (detail / hgweb)
25. Added citations (detail / hgweb)
26. Added citations (detail / hgweb)
27. Added refs (detail / hgweb)
28. Added DOIs (detail / hgweb)
29. Added DOIs (detail / hgweb)
30. Added DOIs (detail / hgweb)
31. Added DOI (detail / hgweb)
32. Added DOI (detail / hgweb)
33. added DOI (detail / hgweb)
34. Median_Method: Add a tight version of the median bound, suggested by Yong Kiam Tan. (detail / hgweb)
35. parse proper toml syntax; (detail / hgweb)
36. Syntax for symmetric set difference, plus tidying (detail / hgweb)
37. Update (detail / hgweb)
38. Update (detail / hgweb)
39. Add (detail / hgweb)
40. Update (detail / hgweb)
41. Update (detail / hgweb)
42. merged (detail / hgweb)
43. Three_Squares: time limit increase; and now sym_diff is declared in main HOL (detail / hgweb)
44. moved Subterm_and_Context into First_Order_Terms, merged context of Term_Aux into Term (detail / hgweb)
45. replace scala.sys.process with proper Bash.Process; (detail / hgweb)
46. renamed "flatten" to "unindex" (detail / hgweb)
47. Resolved some operator clashes (detail / hgweb)
48. merged (detail / hgweb)
49. simplified some proofs (detail / hgweb)
50. Modifications for moving from f ` S <= T to f:S->T (detail / hgweb)
51. Updated for new HOL-CSP (detail / hgweb)
52. merge (detail / hgweb)
53. updated ROOT. (detail / hgweb)
54. Registers: Fixed nonterminating subproof (detail / hgweb)
55. Collected changes to Complex_Bounded_Operators AFP entry:
    
    
    Complex_Vector_Spaces.thy
    =========================
    
    New lemmas: clinear_scaleR[simp], abs_summable_on_scaleC_left[intro],
                abs_summable_on_scaleC_right[intro], ccspan_superset',
                ccspan_closure[simp], ccspan_finite, ccspan_UNIV[simp],
                infsum_in_closed_csubspaceI,
                closed_csubspace_space_as_set[simp], SUP_ccspan
    
    Renamed lemma: bounded_clinear_eq_on -> bounded_clinear_eq_on_closure
    
    Changed typeclass: basis_enum (has additional constant "canonical_basis_length")
    
    Renamed definition: Abs_clinear_space -> Abs_ccsubspace
    
    
    
    Complex_Inner_Product.thy
    =========================
    
    New lemmas: mem_ortho_ccspanI, basis_projections_reconstruct_has_sum,
                basis_projections_reconstruct,
                basis_projections_reconstruct_summable,
                parseval_identity_has_sum, parseval_identity_summable,
                parseval_identity, canonical_basis_is_onb[simp]
    
    
    
    Complex_Bounded_Linear_Functions.thy
    ====================================
    
    New definition: invertible_cblinfun (operator has with left inverse)
    
    New lemmas: not_not_singleton_cblinfun_zero,
                cblinfun_norm_approx_witness', summable_on_cblinfun_apply,
                summable_on_cblinfun_apply_left,
                abs_summable_on_cblinfun_apply_left,
                infsum_cblinfun_apply_left, has_sum_cblinfun_apply_left,
                bounded_clinear_cblinfun_compose_left,
                bounded_clinear_cblinfun_compose_right,
                clinear_cblinfun_compose_left,
                clinear_cblinfun_compose_right,
                additive_cblinfun_compose_left[simp],
                additive_cblinfun_compose_right[simp],
                isCont_cblinfun_compose_left,
                isCont_cblinfun_compose_right, cspan_compose_closed,
                cspan_adj_closed, unitaryI, norm_isometry_compose',
                unitary_nonzero[simp], isometry_inj, unitary_adj_inv,
                isometry_cinner_both_sides, isometry_image_is_ortho_set,
                cblinfun_apply_in_image', cblinfun_image_ccspan_leqI,
                cblinfun_same_on_image, lift_cblinfun_comp,
                cblinfun_image_def2, unitary_image_onb,
                sandwich_arg_compose, sandwich_compose,
                inj_sandwich_isometry, sandwich_isometry_id,
                is_Proj_id[simp], norm_is_Proj_nonzero,
                Proj_compose_cancelI, space_as_setI_via_Proj,
                unitary_image_ortho_compl, Proj_on_image[simp],
                kernel_apply_self, leq_kernel_iff, cblinfun_image_kernel,
                cblinfun_image_kernel_unitary, kernel_cblinfun_compose,
                eigenspace_0[simp], kernel_isometry,
                cblinfun_image_eigenspace_isometry,
                cblinfun_image_eigenspace_unitary, kernel_member_iff,
                kernel_square[simp], cblinfun_inv_left,
                inv_cblinfun_invertible, cblinfun_inv_right,
                iso_cblinfun_unitary, invertible_cblinfun_isometry,
                summable_cblinfun_apply_invertible,
                infsum_cblinfun_apply_invertible, less_eq_scaled_id_norm,
                butterflies_sum_id_finite, butterfly_sum_left,
                butterfly_sum_right, cblinfun_extension_exists_restrict
    
    Changed lemmas: cblinfun_image_INF_eq_general, cblinfun_image_INF_eq
                    (more general), positive_hermitianI (flipped sides of
                    equality), rank1_compose_right, rank1_uminus,
                    rank1_uminus_iff (more general type class)
    
    Removed lemma: dense_span_separating (use
                   bounded_clinear_eq_on_closure instead)
    
    Removed bundles: blinfun_notation, no_blinfun_notation
    
    
    
    Complex_L2.thy
    ==============
    
    New lemmas: clinear_Rep_ell2[simp], Abs_ell2_inverse_finite[simp],
                norm_ell2_bound_trunc, bounded_clinear_Rep_ell2,
                trunc_ell2_singleton, trunc_ell2_insert,
                trunc_ell2_finite_sum, is_orthogonal_trunc_ell2,
                ell2_decompose_has_sum, ell2_decompose_infsum,
                ell2_decompose_summable, Rep_ell2_cblinfun_apply_sum,
                explicit_cblinfun_exists,
                explicit_cblinfun_exists_bounded,
                explicit_cblinfun_exists_finite_dim[simp],
                explicit_cblinfun_ket,
                Rep_ell2_explicit_cblinfun_ket[simp]
    
    Changed lemmas: cinner_ket (uses "of_bool" instead of "if")
    
    Changed definition: ket (uses "of_bool" instead of "if")
    
    New definition: explicit_cblinfun (define an operator by giving the
                    entries of an infinite matrix)
    
    
    
    Cblinfun_Code:
    ==============
    
    New definition: butterfly_code
    
    New lemma: butterfly_code
    
    Renamed definition: cblinfun_apply_code -> cblinfun_apply_ell2
    
    Renamed lemmas:
    - vec_of_ell2_timesScalarVec -> vec_of_ell2_scaleC
    - cinner_ell2_code' -> cinner_ell2_code
    - times_ell2_code' -> times_ell2_code
    - divide_ell2_code' -> divide_ell2_code
    - inverse_ell2_code' -> inverse_ell2_code
    - one_ell2_code' -> one_ell2_code
    - cblinfun_apply_code -> cblinfun_apply_ell2
    - cblinfun_apply_code -> cblinfun_apply_ell2
    
    
    
    
    Cblinfun_Matrix.thy
    ===================
    
    New lemmas: vec_of_basis_enum_carrier_vec, cblinfun_of_mat_invalid
    
    
    
    extra/Extra_General.thy
    =======================
    
    New lemmas: not_not_singleton_zero, has_sumI_metric,
                limitin_pullback_topology, tendsto_coordinatewise,
                limitin_closure_of
    
    
    
    extra/Extra_Vector_Spaces.thy
    =============================
    
    New lemmas: summable_on_bounded_linear, any_norm_exists,
                abs_summable_on_scaleR_left[intro],
                abs_summable_on_scaleR_right[intro],
    
    Changed lemma: enum_idx_bound (expressed using CARD, added [simp])
    
    
    
    extra/Extra_Jordan_Normal_Form.thy
    ==================================
    
    New lemmas: map_map_vec_cols, map_vec_conjugate (detail / hgweb)
56. Renamings of operators, and a major theorem on distributivity of Mprefix vs Sync. Renamings of some lemmata. (detail / hgweb)
57. Updated metadata for several entries.
    
    - Updated categorization for derandomization libraries, based on the newly introduced CS/Alg./Randomized category.
    - Added related reference for Nils Cremer's Tree Enumeration
    - Removed obsolete comments in Expander Grapgs (detail / hgweb)
58. metadata and sitegen for Directed_Sets (detail / hgweb)
59. new entry: Directed_Sets (detail / hgweb)
60. merge from AFP 2022 (detail / hgweb)
61. metadata and sitegen for Multirelations_Heterogeneous (detail / hgweb)
62. new entry: Multirelations_Heterogeneous (detail / hgweb)
63. adjust Schwartz_Zippel entry
    
    - Use Pi_pmf from HOL-Probability
    - Generalize theorem(s) in example (detail / hgweb)
64. adjusted Simple_Clause_Learning from AFP 2022 to AFP devel (detail / hgweb)
65. adjusted Given_Clause_Loops from AFP 2022 to AFP devel (detail / hgweb)
66. adjusted CommCSL from AFP 2022 to AFP devel (detail / hgweb)
67. adjusted DigitsInBase from AFP 2022 to AFP devel (detail / hgweb)
68. adjusted Schwartz_Zippel from AFP 2022 to AFP devel (detail / hgweb)
69. adjusted TsirelsonBound from AFP 2022 to AFP devel (detail / hgweb)
70. adjusted Tree_Enumeration from AFP 2022 to AFP devel (detail / hgweb)
71. adjusted efficient WPO from AFP 2022 to afp devel (detail / hgweb)
72. merge from afp-2022 (detail / hgweb)
73. New entry Efficient_Weighted_Path_Order (detail / hgweb)
74. add edit mode to afp-submit UI; (detail / hgweb)
75. solved subtle problem with multiple entries and new authors; (detail / hgweb)
76. better error logging; (detail / hgweb)
77. added edit handler to submission app; (detail / hgweb)
78. added frontend in devel mode; (detail / hgweb)
79. tuned (mostly api path handling); (detail / hgweb)
80. A real title in place of MLSS_Decision_Proc (detail / hgweb)
81. MLSS_Decision_Proc sitegen (detail / hgweb)
82. New entry MLSS_Decision_Proc (detail / hgweb)
83. metadata and sitegen for TsirelsonBound (detail / hgweb)
84. new entry: TsirelsonBound (detail / hgweb)
85. New entry Tree_Enumeration (detail / hgweb)
86. Three_Squares citegen (detail / hgweb)
87. New entry Three_Squares (detail / hgweb)
88. fixed some ACM/AMS categories (detail / hgweb)
89. more files (detail / hgweb)
90. New entry MHComputation (detail / hgweb)
91. make index.json files line-by-line for smaller diffs; (detail / hgweb)
92. cleanup; (detail / hgweb)
93. added new entry DigitsInBase; (detail / hgweb)
94. fixed broken LaTeX quotation marks in abstracts (detail / hgweb)
95. recategorised some entries (detail / hgweb)
96. new topic: Computer science/Algorithms/Randomized (detail / hgweb)
97. sitegen for Schwartz_Zippel (detail / hgweb)
98. new entry: Schwartz_Zippel (detail / hgweb)
99. New entry: Simple_Clause_Learning (detail / hgweb)
100. New entry HyperHoareLogic (detail / hgweb)
101. New entry Distributed_Distinct_Elements (detail / hgweb)
102. metadata for CommCSL + sitegen (detail / hgweb)
103. new entry: CommCSL (detail / hgweb)
104. New entry No_FTL_observers_Gen_Rel (detail / hgweb)
105. added new files generated by sitegen (detail / hgweb)
106. sitegen (detail / hgweb)
107. metadata for Expander Graphs (detail / hgweb)
108. new entry: Expander Graphs (detail / hgweb)
109. tuned; (detail / hgweb)
110. fix of toml-entries and rerun of sitegen: problem: links where in these quotes: ”...” and not in the standard ones "..." (detail / hgweb)
111. sitegen (for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection) (detail / hgweb)
112. metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection (detail / hgweb)
113. new entry: Two_Generated_Word_Monoids_Intersection (detail / hgweb)
114. new entry: Binary_Code_Imprimitive (detail / hgweb)
115. running sort on ROOTS (detail / hgweb)
116. New entry Probability_Inequality_Completeness (detail / hgweb)
117. Rensets metadata (detail / hgweb)
118. New entry Rensets (detail / hgweb)
119. more Edwards (detail / hgweb)
120. New entry Edwards_Elliptic_Curves_Group (detail / hgweb)
121. metadata and sitegen for CVP_Hardness (detail / hgweb)
122. new entry: CVP_Hardness (detail / hgweb)
123. rerun sitegen (detail / hgweb)
124. revert proof compression experiment (detail / hgweb)
125. metadata for ABY3_Protocols (detail / hgweb)
126. new entry ABY3_Protocols (detail / hgweb)
127. sitegen for Given_Clause_Loops (detail / hgweb)
128. New entry Given_Clause_Loops (detail / hgweb)
129. Adjustments for the simplified version of real_le_lsqrt (detail / hgweb)
130. adapted to Isabelle/84a7a0029c82 (detail / hgweb)
131. merged (detail / hgweb)
132. adapted to Isabelle/0252d635bfb2 (detail / hgweb)
133. merge (detail / hgweb)
134. merge (detail / hgweb)
135. Merge with developper version on LISN gut (detail / hgweb)
136. merged (detail / hgweb)
137. prefer @{attributes} antiquotation over Attrib.internal;
     adapted to Isabelle/bc42c074e58f; (detail / hgweb)
138. tuned proofs; (detail / hgweb)
139. Deleted a superfluous assumption. This proof is a horror (detail / hgweb)
140. merged (detail / hgweb)
141. fixed some bibliographic entries (detail / hgweb)
142. merged (detail / hgweb)
143. tuned (detail / hgweb)
144. merged (detail / hgweb)
145. merged (detail / hgweb)
146. adapted to current Isabelle/ec1c0daa3fbd; (detail / hgweb)
147. adapted to current Isabelle/ec1c0daa3fbd; (detail / hgweb)
148. adapted to Isabelle/5edd5b12017d; (detail / hgweb)
149. proper morphism context; (detail / hgweb)
150. backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531; (detail / hgweb)
151. proper morphism context; (detail / hgweb)
152. adapted to Isabelle/5ab5add88922; (detail / hgweb)
153. SMT-LIB interpretation of floating-point arithmetic (detail / hgweb)
154. merged (detail / hgweb)
155. SMT-LIB interpretation of floating-point arithmetic (detail / hgweb)
156. IEEE model with a single NaN value (detail / hgweb)
157. Minor (detail / hgweb)
158. merging (detail / hgweb)
159. updates for future formalizations (detail / hgweb)
160. adapted to Isabelle/f78cdc6fe971; (detail / hgweb)
161. adapted to Isabelle/f78cdc6fe971; (detail / hgweb)
162. A slight beautification (detail / hgweb)
163. adapted to 3f354d5bbf98; (detail / hgweb)
164. Rounding modes renamed (detail / hgweb)
165. merged (detail / hgweb)
166. Add the rounding mode roundNearestTiesToAway. (detail / hgweb)
167. Merge realtime deque renamings (detail / hgweb)
168. simplify some measurements (detail / hgweb)
169. rename Deque.Idle to Idles (detail / hgweb)
170. Rename Big and Small cases (detail / hgweb)
171. rename `Transforming` to `Rebal` (detail / hgweb)
172. rename `Common.state` to `common_state` (detail / hgweb)
173. rename Small.state to small_state (detail / hgweb)
174. rename Big.state to big_state (detail / hgweb)
175. backed out changeset 2ecb8f5e085f: obsolete thanks to Isabelle/21cdcd120a78; (detail / hgweb)
176. more robust: make it work with Isabelle/a12c48fbf10f; (detail / hgweb)
177. adapted to Isabelle/c4677a6aae2c; (detail / hgweb)
178. adapted to Isabelle/c4677a6aae2c; (detail / hgweb)

Started by an SCM change

This run spent:

• 7.1 sec waiting;
• 4 hr 44 min build duration;
• 4 hr 44 min total from scheduled to completion.