#30 (Sep 29, 2023, 3:18:42 PM)

1. merged (detail / hgweb)
2. adjust Euler_Polyhedron_Formula to AFP-devel (detail / hgweb)
3. merge from AFP 2023 (detail / hgweb)
4. sitegen (detail / hgweb)
5. corrected metadata: doi -> acm identifier (detail / hgweb)
6. metadata for Lovasz_Local and Hypergraph_Basics (detail / hgweb)
7. new entry: Lovasz_Local (detail / hgweb)
8. new entry: Hypergraphs (detail / hgweb)
9. metadata and sitegen for Euler Polyhedron Formula (detail / hgweb)
10. new entry: Euler's Polyhedron Formula (detail / hgweb)
11. adapted to Isabelle/72631efa3821; (detail / hgweb)
12. avoid deadly "handle _ => ..."; (detail / hgweb)
13. tuned: prefer try-catch/finally over low-level 'handle'; (detail / hgweb)
14. tuned: prefer try-catch/finally over low-level 'handle'; (detail / hgweb)
15. tuned: prefer try-catch/finally over low-level 'handle'; (detail / hgweb)
16. clarified signature, following Isabelle/fde0b195cb7d; (detail / hgweb)
17. reduced prominence of lemma names (detail / hgweb)
18. merge from afp-2023 (detail / hgweb)
19. regen website (detail / hgweb)
20. sync web abstract (detail / hgweb)
21. adapted ROOT file link to afp-2023; (detail / hgweb)
22. merge from afp-2023 (detail / hgweb)
23. web: 2023 downlaod links (detail / hgweb)
24. Added tag Isabelle2023 for changeset 01bf5fad3e59 (detail / hgweb)
25. add 2023 release dates (detail / hgweb)
26. website regen (detail / hgweb)
27. fix toml key generated by afp_releases (detail / hgweb)
28. set Isabelle2023 release date (detail / hgweb)
29. update Isabelle2022 release dates (detail / hgweb)
30. afp release path has changed on isa-afp.org (detail / hgweb)
31. fix afp-submit for markdown processing (detail / hgweb)
32. Moved a general purpose theorem into the main repository (detail / hgweb)
33. a little fix involving the reformulated version of inclusion/exclusion (detail / hgweb)
34. fixed missing parenthesis in or-ok-lemma (detail / hgweb)
35. new bibiten and titlecase on all sections (detail / hgweb)
36. avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated operation; (detail / hgweb)
37. replace underscore latex package with formal markup (detail / hgweb)
38. merge (detail / hgweb)
39. fix latex generation (detail / hgweb)
40. Backed out changeset 8eb0a45852dc (detail / hgweb)
41. tuned; (detail / hgweb)
42. avoid non-local return; (detail / hgweb)
43. removed migration tools; (detail / hgweb)
44. follow naming conventions of Isabelle/2a99fcb283ee; (detail / hgweb)
45. adapted to Isabelle/fd1fec53665b; (detail / hgweb)
46. Relational_Disjoint_Set_Forests: update history (detail / hgweb)
47. Relational_Disjoint_Set_Forests: minor text edits (detail / hgweb)
48. merged (detail / hgweb)
49. small fixes (detail / hgweb)
50. fix afp-submit for markdown processing (detail / hgweb)
51. switch version back to devel after fork (detail / hgweb)
52. use default AFP chapter settings (detail / hgweb)
53. merge from afp-devel (detail / hgweb)
54. update version to 2023 (detail / hgweb)
55. update author email (by request) (detail / hgweb)
56. Tree_Enumeration: Fix errors introduced by renamings in Unidrected_Graph_Theory. (detail / hgweb)
57. merge from afp-2022 (detail / hgweb)
58. sitegen for Fixed_Length_Vector (detail / hgweb)
59. added syntax bundles and disabled syntax by default (detail / hgweb)
60. moved abstract to root.tex (detail / hgweb)
61. made proofs more robust (detail / hgweb)
62. new entry Fixed_Length_Vector (detail / hgweb)
63. Fixed the title and author of Ceva in the document (detail / hgweb)
64. sitegen for Ceva (detail / hgweb)
65. new entry Ceva (detail / hgweb)
66. for better output notation (detail / hgweb)
67. regen website (detail / hgweb)
68. fix duplicated key in IEEE_Floating_Point.toml (detail / hgweb)
69. Merge changes (detail / hgweb)
70. Renamed incident and order to vincident and gorder due to` compatibility issues. (detail / hgweb)
71. Note recent additions (roundNearestTiesToAway, single NaN value, SMT-LIB translation) in metadata. (detail / hgweb)
72. Merged. (detail / hgweb)
73. Registers: Fixed some broken proofs. (detail / hgweb)
74. redefine substitution of terms as special case of general evaluation of terms (detail / hgweb)
75. Complex_Bounded_Operators: Various changes:
    
    - Code generation support for `explicit_cblinfun`.
    - Various changes and additions in `Cblinfun_Matrix` and `Cblinfun_Code`
    - Lemma `sandwich_compose`: Switched lhs and rhs.
    - New lemmas `is_ortho_set_prod`, `ccsubspace_Times_ccspan`.
    - Definition `cblinfun_inv`: Default value 0 when inverse does not exist.
    - Renamed `riesz_frechet_representation_...` -> `riesz_representation_...`.
    - Generalized lemma `inj_ket`. (detail / hgweb)
76. update author info (detail / hgweb)
77. Update of Combinatorics_Words, Combinatorics_Words_Graph_Lemma, Combinatorics_Words_Lyndon, Two_Generated_Word_Monoids_Intersection, Binary_Code_Imprimitive to to version v1.10. (detail / hgweb)
78. metadata formatting (detail / hgweb)
79. address metadata warnings (detail / hgweb)
80. merge from afp-2022 (detail / hgweb)
81. remove unused metadata (leaves website unchanged) (detail / hgweb)
82. new entry Catoids (detail / hgweb)
83. remove obsolete (AFP) group from new entries (detail / hgweb)
84. Word_Lib: import new material from l4v (detail / hgweb)
85. update to isabelle@fd8e1bbc0686 (detail / hgweb)
86. merge from afp-2022 (detail / hgweb)
87. merge from afp-2022 (detail / hgweb)
88. New entry Polygonal_Number_Theorem (detail / hgweb)
89. Quantales_Converse metadata (detail / hgweb)
90. new entry Quantales_Converse (detail / hgweb)
91. Fixed the punctuation in the title and abstract (detail / hgweb)
92. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser (detail / hgweb)
93. New entry /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser (detail / hgweb)
94. regenerate site; (detail / hgweb)
95. tuned links in theory view; (detail / hgweb)
96. tuned instructions; (detail / hgweb)
97. regenerate site; (detail / hgweb)
98. clarify statistics-ignore flag and build example submission properly; (detail / hgweb)
99. regen website (detail / hgweb)
100. rectify copy/paste error (detail / hgweb)
101. merged (detail / hgweb)
102. Redid an ugly proof (detail / hgweb)
103. construction for anchord GTT intersection
     
     by Alexander Lochman (detail / hgweb)
104. merged (detail / hgweb)
105. Updated the root file to start from an AFP image (detail / hgweb)
106. tuned (detail / hgweb)
107. merged (detail / hgweb)
108. new editors Lammich and Traytel (detail / hgweb)
109. Eliminated needless import and rationalised the ROOT file (detail / hgweb)
110. Deleted needless imports (detail / hgweb)
111. Generalised and tidied an intermediate result (detail / hgweb)
112. Higher_Order_Terms: add fresh_list function (detail / hgweb)
113. delete unneeded file (detail / hgweb)
114. antiquoting special symbols in text (detail / hgweb)
115. merge with default (detail / hgweb)
116. Relational_Disjoint_Set_Forests: extended theory, refactored related entries (detail / hgweb)
117. Refactored and updated entry. Synchronize with companion paper. (detail / hgweb)
118. simplified proof without auxiliary function (detail / hgweb)
119. provide more unification algorithms, e.g., to compute mgu's modulo variable renamings (detail / hgweb)
120. Adapted to devel (detail / hgweb)
121. Relational_Disjoint_Set_Forests: simplified invariant (detail / hgweb)
122. Bell_Numbers_Spivey: Add code equations for the computation of Bell numbers. (detail / hgweb)
123. Distributed_Distinct_Elements: Swap epsilon/delta for the spec of the algorithm.
     
     The reason is to preserve consistency with the upcoming publication to appear at RANDOM 2023. (detail / hgweb)
124. proved a few properties of WPO with less assumption, so that Co-WPO properties can be derived (detail / hgweb)
125. Fixed LaTeX. (detail / hgweb)
126. Merge. (detail / hgweb)
127. Fixed missing entries in ROOTS file (previous erronous commit). (detail / hgweb)
128. Normalised email. (detail / hgweb)
129. Improved setup of the symbolic evaluator. (detail / hgweb)
130. Fix proofs broken by previous commit. (detail / hgweb)
131. Universal_Hash_Families: Avoid using non-descriptive theory names.
     
     Note: The namespace for theory names is global, i.e., a name like "Definitions" is likely to cause collisions. (detail / hgweb)
132. merged (detail / hgweb)
133. Adjustments for recent cosmetic changes to the Distribution (detail / hgweb)
134. Proper epsilon-syntax (detail / hgweb)
135. Merge. (detail / hgweb)
136. Minor improvement of handling of string literals in symbolic evaluator. (detail / hgweb)
137. Removing redundant definitions:
     - External
     - Fallback (detail / hgweb)
138. tuned (detail / hgweb)
139. Merge (detail / hgweb)
140. Updating history for Isabelle/Solidity (detail / hgweb)
141. Updating Isabelle/Solidity:
     - Changing expressions do not have side effects anymore.
     - Adding support for instantiation of contracts.
     - Adding weakest precondition calculus for the verification of statements. (detail / hgweb)
142. Relational_Disjoint_Set_Forests: added a new theory, refactored related entries (detail / hgweb)
143. remove some redundant constraint-types in simplex algorithm (detail / hgweb)
144. relation between has-maximum and bdd_above (detail / hgweb)
145. tuned names (detail / hgweb)
146. merged (detail / hgweb)
147. more comments (detail / hgweb)
148. merged (detail / hgweb)
149. back out Paraconsistency (detail / hgweb)
150. merged (detail / hgweb)
151. tuned and simplified proofs (detail / hgweb)
152. Some additions to IICF by Valentin Springsklee (detail / hgweb)
153. merge (detail / hgweb)
154. small changes in FOL_Seq_Calc1 metadata (detail / hgweb)
155. More Paraconsistency (detail / hgweb)
156. merged (detail / hgweb)
157. tuned (detail / hgweb)
158. tuned (detail / hgweb)
159. prefer existing Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail / hgweb)
160. proper .ML file names; (detail / hgweb)
161. proper .ML file name; (detail / hgweb)
162. eliminated suspicious Unicode character, which often produce unexpected document output; (detail / hgweb)
163. eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail / hgweb)
164. tuned whitespace; (detail / hgweb)
165. avoid hardwired document output; (detail / hgweb)
166. eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail / hgweb)
167. tuned signature; (detail / hgweb)
168. fixed build following a13761ef6796 (detail / hgweb)
169. merged (detail / hgweb)
170. removed unnecessary theory with potential for name conflict (detail / hgweb)
171. provided var2-versions of all doubly-nested loops (detail / hgweb)
172. Added version of algorithm 4 with precise variant var2 and tuned (detail / hgweb)
173. Floyd Warshall: improve code refinements (detail / hgweb)
174. IMP2: fix typos (detail / hgweb)
175. New check 'coverage_rcv' added. (detail / hgweb)
176. Fixing typos. (detail / hgweb)
177. Updated formalization to include improvements described in the
     following publication:
     
          Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker.
          2023. Stateful Protocol Composition in Isabelle/HOL. ACM Trans.
          Priv. Secur. 26, 3, Article 25 (August 2023), 36 pages.
          https://doi.org/10.1145/3577020 (detail / hgweb)
178. typos (detail / hgweb)
179. remove AFP group already defined by chapter; (detail / hgweb)
180. Sync with my development repo. (detail / hgweb)

Started by an SCM change

This run spent:

• 3 hr 54 min waiting;
• 4 hr 37 min build duration;
• 8 hr 32 min total from scheduled to completion.