Skip to content

Changes

#34 (Mar 27, 2024, 10:09:14 PM)

  1. proper Go setup, following Isabelle/1e7d4372fe3d; — wenzelm / hgweb
  2. tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  3. tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  4. tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  5. tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  6. tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  7. updates to new time function generator that now translates undefined to undefined, not 0 — nipkow / hgweb
  8. Fixes mostly for log_mono aliasing — paulson <lp15@cam.ac.uk> / hgweb
  9. Brought this new entry up-to-date with the development version — paulson <lp15@cam.ac.uk> / hgweb

#33 (Mar 26, 2024, 9:21:19 PM)

  1. merged — Lars Hupel <lars@hupel.info> / hgweb
  2. sitegen for Continued_Fractions — paulson <lp15@cam.ac.uk> / hgweb
  3. New entry "Continued_Fractions" — paulson <lp15@cam.ac.uk> / hgweb
  4. sitegen for Approximate_Model_Counting — traytel / hgweb
  5. tuned (removing warnings) — traytel / hgweb
  6. new entry Approximate_Model_Counting — traytel / hgweb
  7. Go: website updates — Peter Lammich / hgweb
  8. Go submission — Peter Lammich / hgweb
  9. adapt to Isabelle/11a1f4d7af51; — Fabian Huch <huch@in.tum.de> / hgweb
  10. use emph instead of italic; — Fabian Huch <huch@in.tum.de> / hgweb
  11. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  12. clarified names; — Fabian Huch <huch@in.tum.de> / hgweb
  13. tuned lemmas — desharna / hgweb
  14. merged — desharna / hgweb
  15. removed stuff moved to the Isabelle distribution — desharna / hgweb
  16. avoid java.net.URL, following Isabelle/a4118f530263; — Fabian Huch <huch@in.tum.de> / hgweb
  17. updated: standard Borel — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
  18. use time_fun command — nipkow / hgweb
  19. merged — nipkow / hgweb
  20. Splay tree analysis now uses time_fun command — nipkow / hgweb
  21. tuned proofs to reduce verification time following Isabelle/7735645667f0 — desharna / hgweb
  22. merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  23. feat(Transport) major improvement of overloaded properties + new relational properties — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  24. fix(ML_Unification) replace binders before aeconv (avoids lowering) — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  25. feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  26. merged — desharna / hgweb
  27. adapted to new definition of wf following Isabelle/033f90dc441d — desharna / hgweb
  28. merged — paulson / hgweb
  29. Two new lemmas by Eberl (requested by Paulson) — paulson <lp15@cam.ac.uk> / hgweb
  30. adapted to isabelle/devel — nipkow / hgweb
  31. adapted to new definition of wfP following Isabelle/233d70cad0cf — desharna / hgweb
  32. updated url — nipkow / hgweb
  33. merged — desharna / hgweb
  34. tuned proof — desharna / hgweb
  35. Patching some proofs, for of_nat_int_ceiling — paulson <lp15@cam.ac.uk> / hgweb
  36. Deletion of material that had been moved to the distribution — paulson <lp15@cam.ac.uk> / hgweb
  37. Multirelations_Heterogeneous: further results for convex-closure — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  38. added some material about the Laurent expansion of zeta — Manuel Eberl <manuel@pruvisto.org> / hgweb
  39. Remove stuff following Isabelle/d0205dde00bb and related changesets — desharna / hgweb
  40. fixed broken definitions and proofs following Isabelle/8d153846f65f — desharna / hgweb
  41. Universal_Hash_Families: Remove accidental duplication of pmf_of_set_prod_eq. — Emin Karayel <me@eminkarayel.de> / hgweb
  42. Inserted a corollary to the main result — paulson <lp15@cam.ac.uk> / hgweb
  43. Updated a proof to the new formalisation of meromorphic — paulson <lp15@cam.ac.uk> / hgweb
  44. Relational_Cardinality: minor revision — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  45. adapted to Isabelle/2746dfc9ceae; — wenzelm / hgweb
  46. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  47. adjusting HOL-CSP_OpSem from 2023 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  48. merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  49. metadata for HOL-CSP OpSem and sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  50. new entry: HOL-CSP OpSem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  51. removed lemmas following Isabelle/ba8fb71587ae — desharna / hgweb
  52. merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  53. sitegen for Wieferich Kempner — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  54. new entry: Wieferich Kempner — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  55. merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  56. metadata and sitegen for QBF-Solver — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  57. new entry: QBF_Solver_Verification — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  58. further files for CubicalCategories — nipkow / hgweb
  59. New entry CubicalCategories — nipkow / hgweb
  60. update doc; — Fabian Huch <huch@in.tum.de> / hgweb
  61. Correction of an error in the abstract — paulson <lp15@cam.ac.uk> / hgweb
  62. sitegen for Karatsuba — paulson <lp15@cam.ac.uk> / hgweb
  63. New submission: Karatsuba — paulson <lp15@cam.ac.uk> / hgweb
  64. adjusted proof — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  65. more accurate timeout;
    tuned whitespace; — wenzelm / hgweb
  66. move multiset lemmas into distro — blanchet / hgweb
  67. non-executable files; — wenzelm / hgweb
  68. Moving library material into Analysis (Elementary_Metric_Spaces and Set_Integration) — paulson <lp15@cam.ac.uk> / hgweb
  69. New version consistent with paper — nipkow / hgweb
  70. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  71. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  72. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  73. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  74. tuned whitespace; — wenzelm / hgweb
  75. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
  76. tuned whitespace; — wenzelm / hgweb
  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; — wenzelm / hgweb
  78. tuned signature, following Isabelle/da4e82434985; — wenzelm / hgweb
  79. adapted to Isabelle/3648e9c88d0c; — Fabian Huch <huch@in.tum.de> / hgweb
  80. Fixed a rewriting issue — paulson <lp15@cam.ac.uk> / hgweb
  81. Resolved a syntax clash involving Equipollence (now imported by Ramsey) — paulson <lp15@cam.ac.uk> / hgweb
  82. enable proof in session Lorenz_C1 — immler / hgweb
  83. simplified proofs — blanchet / hgweb
  84. simplified proof — blanchet / hgweb
  85. Incorporating library material from AFP sessions — paulson <lp15@cam.ac.uk> / hgweb
  86. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic — blanchet / hgweb
  87. merged — paulson / hgweb
  88. Removed numerous z3 calls and tried to simplify some extremely messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  89. Adjustments for recent changes to the main repository — paulson <lp15@cam.ac.uk> / hgweb
  90. A little tidying up. Removed some smt calls — paulson <lp15@cam.ac.uk> / hgweb
  91. avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic — blanchet / hgweb
  92. tuned proofs — blanchet / hgweb
  93. Simpl: remove stray thm command — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  94. CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218fa — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  95. Interval_Analysis: adapt to isabelle@cff4576218fa — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  96. merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  97. update Simpl entry; change license to BSD

    (submission by Norbert Schirmer) — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  98. sitegen for IMP_Noninterference — paulson <lp15@cam.ac.uk> / hgweb
  99. New entry IMP_Noninterference — paulson <lp15@cam.ac.uk> / hgweb
  100. sitegen for Sumcheck Protocol — traytel / hgweb
  101. new entry Sumcheck Protocol — traytel / hgweb
  102. New entry OmegaCatoidsQuantales — nipkow / hgweb
  103. New submission Region_Quadtrees — paulson <lp15@cam.ac.uk> / hgweb
  104. sitegen and metadata for Isabelle_hoops — paulson <lp15@cam.ac.uk> / hgweb
  105. New entry Isabelle_hoops (with its name standardised) — paulson <lp15@cam.ac.uk> / hgweb
  106. sitegen and metadata for Interval_Analysis — paulson <lp15@cam.ac.uk> / hgweb
  107. New submission Interval_Analysis — paulson <lp15@cam.ac.uk> / hgweb
  108. New entry CRYSTALS-Kyber_Security — nipkow / hgweb
  109. proper Homepage comparison: URL equals does not fulfil specification; — Fabian Huch <huch@in.tum.de> / hgweb
  110. A lot of tidying — paulson <lp15@cam.ac.uk> / hgweb
  111. merged — paulson / hgweb
  112. Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  113. Cleaning and simplifying notation — carolos@live.nl / hgweb
  114. A little tidying. Removal of z3 smt calls — paulson <lp15@cam.ac.uk> / hgweb
  115. formally normalized definition of singleton shifts to their primitive form — haftmann / hgweb
  116. Integration syntax — paulson <lp15@cam.ac.uk> / hgweb
  117. Importation of the infinite type class — paulson <lp15@cam.ac.uk> / hgweb
  118. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now  requires parentheses — paulson <lp15@cam.ac.uk> / hgweb
  119. Moving a few facts from libraries into the main repository — paulson <lp15@cam.ac.uk> / hgweb
  120. Shortening some proofs — carolos@live.nl / hgweb
  121. Correcting misleading notation — carolos@live.nl / hgweb
  122. simplified class specification — haftmann / hgweb
  123. more realistic timeouts; — wenzelm / hgweb
  124. Borrowed prod_mono_strict' for the distribution; adjusted proofs — paulson <lp15@cam.ac.uk> / hgweb
  125. merged — desharna / hgweb
  126. added lifting of forward simulation to transitive closure — desharna / hgweb
  127. Renamed a theorem involving convexity — paulson <lp15@cam.ac.uk> / hgweb
  128. Updated a proof for the corrected version of convex_on — paulson <lp15@cam.ac.uk> / hgweb
  129. Made the proof slightly more explicit — paulson <lp15@cam.ac.uk> / hgweb
  130. Fixed a problem involving sum_diff_split — paulson <lp15@cam.ac.uk> / hgweb
  131. New lemmas and renaming of lemmas — paulson <lp15@cam.ac.uk> / hgweb
  132. feat(ML_Unification,Transport) more robust unification + new unifiers — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  133. strengthened class parity — haftmann / hgweb
  134. "Moving up" AFP library material to more appropriate places — paulson <lp15@cam.ac.uk> / hgweb
  135. merged — paulson / hgweb
  136. Simplification of some of the lemma libraries — paulson <lp15@cam.ac.uk> / hgweb
  137. merged — nipkow / hgweb
  138. use define_time_function — nipkow / hgweb
  139. common type class for trivial properties on div/mod — haftmann / hgweb
  140. Expander_Graphs: Add additional tail bound for expander random walks. — Emin Karayel <me@eminkarayel.de> / hgweb
  141. rearranged and reformulated abstract classes for bit structures and operations — haftmann / hgweb
  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). — Emin Karayel <me@eminkarayel.de> / hgweb
  143. tuned signature; — wenzelm / hgweb
  144. adapted to Isabelle/c7a98469c0e7; — wenzelm / hgweb
  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. — Emin Karayel <me@eminkarayel.de> / hgweb
  146. merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  147. feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  148. Universal_Hash_Families: Remove duplicate proofs (caused by previous commit.) — Emin Karayel <me@eminkarayel.de> / hgweb
  149. Finite_Fields: Add exectuable algorithms for the construction of (and calculation in) finite fields. — Emin Karayel <me@eminkarayel.de> / hgweb
  150. Finite Fields: Minor improvements to previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
  151. Finite_Fields: Add Rabin's test for the irreducibility of polynomials. — Emin Karayel <me@eminkarayel.de> / hgweb
  152. Finite Fields: Add more general lower estimate for cardinality of irreducible polynomials. — Emin Karayel <me@eminkarayel.de> / hgweb
  153. Distributed_Distinct_Elements: Add related entries. — Emin Karayel <me@eminkarayel.de> / hgweb
  154. Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities. — Emin Karayel <me@eminkarayel.de> / hgweb
  155. Renamed a theorem — paulson <lp15@cam.ac.uk> / hgweb
  156. streamlined type class specification — haftmann / hgweb
  157. consolidated lemma name — haftmann / hgweb
  158. simplified specification of type class — haftmann / hgweb
  159. consolidated name of lemma analogously to nat/int/word_bit_induct — haftmann / hgweb
  160. tuned finite proofs — nipkow / hgweb
  161. merged — wenzelm / hgweb
  162. adapted to Isabelle/7d10708bbc32; — wenzelm / hgweb
  163. adapted to isabelle/devel — nipkow / hgweb
  164. Relational_Disjoint_Set_Forests: minor revision — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  165. more realistic timeout; — wenzelm / hgweb
  166. fix(ML_Unification) use cartouches to fix document build error — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  167. feat(ML_Unification) more explanation — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  168. merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  169. feat(Transport) better relativised concept definitions and lemmas — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  170. feat(ML_Unification) add recursive unification hints fallback option — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  171. CZH_Foundations: integration with Cardinality_Continuum — user9716869 <user9716869@gmail.com> / hgweb
  172. tuned; — wenzelm / hgweb
  173. tuned; — wenzelm / hgweb
  174. adapted to Isabelle/e1895596e1b9; — wenzelm / hgweb
  175. adapted to Isabelle/c6c2e41cac1c; — wenzelm / hgweb
  176. proper terminology; — wenzelm / hgweb
  177. removed outdated comments; — wenzelm / hgweb
  178. adapted to Isabelle/70c0dbfacf0b; — wenzelm / hgweb
  179. tuned; — wenzelm / hgweb
  180. tuned, following Isabelle/8c9cce335a3d; — wenzelm / hgweb
  181. tuned; — wenzelm / hgweb
  182. tuned; — wenzelm / hgweb
  183. tuned; — wenzelm / hgweb
  184. tuned; — wenzelm / hgweb
  185. tuned; — wenzelm / hgweb
  186. tuned, following Isabelle/e7796c55d840; — wenzelm / hgweb
  187. Hello_World: add some descriptive text — Lars Hupel <lars@hupel.info> / hgweb
  188. Introduced definition for the sigma algebra at infinity for a filtration. — Ata Keskin <ata.keskin@tum.de> / hgweb
  189. Fixed issue that caused Martingales to not compile. Sorry! — Ata Keskin <ata.keskin@tum.de> / hgweb
  190. re-introduce code in session of Hello_World — Lars Hupel <lars@hupel.info> / hgweb
  191. adapted to Isabelle/032a31db4c6f; — wenzelm / hgweb
  192. adjusted HOL-CSPM from 2023 to development (Patch.thy might need further cleanup) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  193. Updated entry Martingales. — Ata Keskin <ata.keskin@tum.de> / hgweb
  194. adapted Disintegration to devel — Manuel Eberl <eberlm@in.tum.de> / hgweb
  195. adapted to isabelle-dev; — wenzelm / hgweb
  196. adjusted Concentration Inequalities from 2023 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  197. merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  198. tuned — nipkow / hgweb
  199. New entry KnuthMorrisPratt — nipkow / hgweb
  200. metadata and sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  201. new entry: HOL-CSPM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  202. sitegen for Martingales — Manuel Eberl <eberlm@in.tum.de> / hgweb
  203. new entry Martingales — Manuel Eberl <eberlm@in.tum.de> / hgweb
  204. sitegen for Concentration_Inequalities — Manuel Eberl <eberlm@in.tum.de> / hgweb
  205. new entry Concentration_Inequalities — Manuel Eberl <eberlm@in.tum.de> / hgweb
  206. New entry: Lambert_Series — nipkow / hgweb
  207. adjusted doi capitalization — traytel / hgweb
  208. sitegen for Q0_soundness — traytel / hgweb
  209. new entry Q0_Soundness — traytel / hgweb
  210. sitegen for Cardinality_Continuum — traytel / hgweb
  211. new entry Cardinality_Continuum — traytel / hgweb
  212. Polylog web files — nipkow / hgweb
  213. sitegen for Polylog — nipkow / hgweb
  214. New entry: Polylog — nipkow / hgweb
  215. sitegen for Polynomial_Crit_Geometry — paulson <lp15@cam.ac.uk> / hgweb
  216. new entry Polynomial_Crit_Geometry — paulson <lp15@cam.ac.uk> / hgweb
  217. sitegen for Chebyshev_Polynomials — paulson <lp15@cam.ac.uk> / hgweb
  218. New entry Chebyshev_Polynomials — paulson <lp15@cam.ac.uk> / hgweb
  219. more website for LTL and PD — lammich <lammich@in.tum.de> / hgweb
  220. website for LTL and PD — lammich <lammich@in.tum.de> / hgweb
  221. Labeled_Transition_Systems and Pushdown_Systems — lammich <lammich@in.tum.de> / hgweb
  222. New entry: Nominal_Myhill_Nerode — nipkow / hgweb
  223. more doc; — Fabian Huch <huch@in.tum.de> / hgweb
  224. sitegen for Q0_Metatheory — traytel / hgweb
  225. updated LaTeX citations — traytel / hgweb
  226. new entry Q0_Metatheory — traytel / hgweb
  227. Perfect_Fields and Elimination_Of_Repeated_Factors incl sitegen — paulson <lp15@cam.ac.uk> / hgweb
  228. New entry Perfect_Fields — paulson <lp15@cam.ac.uk> / hgweb
  229. sitegen for /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Disintegration — paulson <lp15@cam.ac.uk> / hgweb
  230. New entry "Disintegration" — paulson <lp15@cam.ac.uk> / hgweb
  231. allow partially detecting potential name conflicts; — Fabian Huch <huch@in.tum.de> / hgweb
  232. added check to detect potential name conflicts; — Fabian Huch <huch@in.tum.de> / hgweb
  233. add warning for missing DOI cache; — Fabian Huch <huch@in.tum.de> / hgweb
  234. Eudoxus_Reals patch and sitegen — paulson <lp15@cam.ac.uk> / hgweb
  235. New entry, Eudoxus_Reals — paulson <lp15@cam.ac.uk> / hgweb
  236. New entry /Hypergraph_Colourings — nipkow / hgweb
  237. adapted to Isabelle/99bc2dd45111; — wenzelm / hgweb
  238. adapted to simplified T convention — nipkow / hgweb
  239. merged — nipkow / hgweb
  240. adapted to new T conventions — nipkow / hgweb
  241. extracted lemma finite_progress out of proof — desharna / hgweb
  242. simplified proof — nipkow / hgweb
  243. merged — desharna / hgweb
  244. tuned lift_strong_simulation_to_bisimulation — desharna / hgweb
  245. simplified definition of match_bisim — desharna / hgweb
  246. strengthened lift_strong_simulation_to_bisimulation and simplified match_bisim — desharna / hgweb
  247. adadpted to [simp] changes in distrib — nipkow / hgweb
  248. de-duplicated specification of class ring_bit_operations — haftmann / hgweb
  249. adjusted T_sift_down: all primitives take 0 time. — nipkow / hgweb
  250. added missing file following 2702f2046afa — desharna / hgweb
  251. documented change in VeriComp — desharna / hgweb
  252. added framework-independent lemma to lift simulation to bisimulation — desharna / hgweb
  253. tuned — nipkow / hgweb
  254. added publication — nipkow / hgweb
  255. slightly more elementary characterization of unset_bit — haftmann / hgweb
  256. base abstract specification of NOT on recursive equation rather than bit projection — haftmann / hgweb
  257. more realistic timeouts for lrzcloud2:threads=1; — Fabian Huch <huch@in.tum.de> / hgweb
  258. tuned proof — haftmann / hgweb
  259. more realistic timeouts for lrzcloud2:threads=1; — wenzelm / hgweb
  260. operations AND, OR, XOR are specified by characteristic recursive equation — haftmann / hgweb
  261. some extensions to Cotangent_PFD_Formula — Manuel Eberl <manuel@pruvisto.org> / hgweb
  262. slightly less technical formulation of very specific type class — haftmann / hgweb

#32 (Nov 6, 2023, 7:33:09 PM)

  1. fixed duplicate theory name in Polynomial_Factorization — Manuel Eberl <eberlm@in.tum.de> / hgweb
  2. refactored proof — traytel / hgweb
  3. merged — paulson / hgweb
  4. Removal of the original and obsolete development; replaced by links to the corresponding theorems in the Isabelle libraries — paulson <lp15@cam.ac.uk> / hgweb
  5. more realistic timeout; — wenzelm / hgweb
  6. proper document setup for \usepackage{times};
    drop extra copy of generated document; — wenzelm / hgweb
  7. more realistic timeout; — wenzelm / hgweb
  8. avoid hardwired document output; — wenzelm / hgweb
  9. merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  10. fix(ML_Unification/Parsing) change map_safe type to return an option — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  11. Fixed issues connected with cong_def vs unique_euclidean_semiring_class.cong_def and := syntax — paulson <lp15@cam.ac.uk> / hgweb
  12. Got rid of some global (and unnecessary) parameter settings. Also fixed a couple of slow proofs — paulson <lp15@cam.ac.uk> / hgweb
  13. feat(ML_Unification) use fixed parser from Isabelle distro — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  14. merged — desharna / hgweb
  15. removed unnecessary condition that decided literals are in N — desharna / hgweb
  16. added name to corollary — desharna / hgweb
  17. removed lemma now in distribution — desharna / hgweb
  18. added lemma right_unique_skip — desharna / hgweb
  19. Stone_Relation_Algebras: minor additions — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  20. merged — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
  21. Standard_Borel_Spaces: removed an unnecessary file — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
  22. Standard_Borel_Spaces and S_Finite_Measure_Monad: adjust theories to metric space in Isabelle2023 — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
  23. remove ci-extras component (see Isabelle/f992769d); — Fabian Huch <huch@in.tum.de> / hgweb
  24. use ci build mail server; — Fabian Huch <huch@in.tum.de> / hgweb
  25. use Isabelle options for CI mail settings (see Isabelle/4c5aadf1); — Fabian Huch <huch@in.tum.de> / hgweb
  26. removed unused/broken clone (see Isabelle/aff231884b20); — wenzelm / hgweb
  27. adaptred to Isabelle/d769a183d51d; — wenzelm / hgweb
  28. more standard simproc_setup using ML antiquotation; — wenzelm / hgweb
  29. adapted to Isabelle/807b249f1061; — wenzelm / hgweb
  30. clarified simproc_setup (passive); — wenzelm / hgweb
  31. avoid clash with outer syntax keyword 'passive'; — wenzelm / hgweb
  32. merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  33. Transport sitegen — paulson <lp15@cam.ac.uk> / hgweb
  34. New submission Transport — paulson <lp15@cam.ac.uk> / hgweb
  35. update S_Finite_Measure_Monad to Isabelle2023 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  36. web pages for Standard_Borel_Spaces and S_Finite_Measure_Monad — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  37. update Standard_Borel_Spaces to Isabelle2023 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  38. theory files for S_Finite_Measure_Monad + Standard_Borel_Spaces — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  39. new entry IO_Language_Conformance — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  40. new entry Coupledsim_Contrasim — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  41. drop SN from standard wpo-assumptions; prove irreflexivity of WPO without SN — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  42. added proof: the multiset extension of two orders preserves irreflexivity — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  43. added lemmas on lexicographic extension — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  44. added code-unfold lemma — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  45. fix(ML_Unification) remove temporary files — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  46. update hugo to 0.119.0; — Fabian Huch <huch@in.tum.de> / hgweb
  47. moved hugo component build tool to Isabelle distribution; — Fabian Huch <huch@in.tum.de> / hgweb
  48. update hugo component and support more platforms; — Fabian Huch <huch@in.tum.de> / hgweb

#31 (Oct 6, 2023, 9:33:16 AM)

  1. merge from afp-2023; — Fabian Huch <huch@in.tum.de> / hgweb
  2. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  3. change web path to /sessions/ instead of /theories/ for consistent naming scheme; — Fabian Huch <huch@in.tum.de> / hgweb
  4. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  5. tuned: remove hugo warnings; — Fabian Huch <huch@in.tum.de> / hgweb
  6. tuned whitespace; — Fabian Huch <huch@in.tum.de> / hgweb
  7. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  8. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  9. display only unique exact matches in topic listing; — Fabian Huch <huch@in.tum.de> / hgweb
  10. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  11. remove automatic title capitalization; — Fabian Huch <huch@in.tum.de> / hgweb
  12. improve description of the submission process; — Fabian Huch <huch@in.tum.de> / hgweb
  13. improved path resolving in theory view; — Fabian Huch <huch@in.tum.de> / hgweb
  14. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  15. generate theory listings for dependencies in distribution; — Fabian Huch <huch@in.tum.de> / hgweb
  16. sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  17. obtain theory html file urls from browser_info instead of hard-coded links; — Fabian Huch <huch@in.tum.de> / hgweb
  18. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  19. tuned whitespace; — Fabian Huch <huch@in.tum.de> / hgweb
  20. record proper entry dependencies instead of relying on coincidental session names; — Fabian Huch <huch@in.tum.de> / hgweb
  21. clarify chapter urls: remove from config as they are a separate concept; — Fabian Huch <huch@in.tum.de> / hgweb
  22. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  23. sitegen — traytel / hgweb
  24. new entry ML_Unification — traytel / hgweb
  25. Inserted another missing acknowledgement — paulson <lp15@cam.ac.uk> / hgweb
  26. fix web; — Fabian Huch <huch@in.tum.de> / hgweb
  27. added missing files — nipkow / hgweb
  28. New entry Relational_Cardinality — nipkow / hgweb
  29. Acknowledging the Alexandria project in two entries — paulson <lp15@cam.ac.uk> / hgweb
  30. Adaption to new HOL-CSP core; some stronger compactification theorems. — Burkhart Wolff <wolff@lri.fr> / hgweb
  31. Integrated many contributions by Benoit Ballenghuin.
    - shorter proofs in CSP
    - theory CSP_Induct
    - theory Renaming
    - updates on documentation — Burkhart Wolff <wolff@lri.fr> / hgweb
  32. merged — nipkow / hgweb
  33. more lit.refs — nipkow / hgweb
  34. Removal of material that had already been migrated to the repository — paulson <lp15@cam.ac.uk> / hgweb
  35. added lit.ref. — nipkow / hgweb
  36. sitegen — nipkow / hgweb
  37. fix link; — Fabian Huch <huch@in.tum.de> / hgweb
  38. sitegen — nipkow / hgweb
  39. fix url/file encoding; — Fabian Huch <huch@in.tum.de> / hgweb
  40. typo — nipkow / hgweb
  41. typo — nipkow / hgweb
  42. tuned metadata — nipkow / hgweb
  43. tuned metadata — nipkow / hgweb
  44. tuned metadata — nipkow / hgweb
  45. merged — paulson / hgweb
  46. Migration of lemmas to distribution — paulson <lp15@cam.ac.uk> / hgweb

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

  1. merged — wenzelm / hgweb
  2. adjust Euler_Polyhedron_Formula to AFP-devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  3. merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  4. sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  5. corrected metadata: doi -> acm identifier — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  6. metadata for Lovasz_Local and Hypergraph_Basics — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  7. new entry: Lovasz_Local — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  8. new entry: Hypergraphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  9. metadata and sitegen for Euler Polyhedron Formula — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  10. new entry: Euler's Polyhedron Formula — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  11. adapted to Isabelle/72631efa3821; — wenzelm / hgweb
  12. avoid deadly "handle _ => ..."; — wenzelm / hgweb
  13. tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
  14. tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
  15. tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
  16. clarified signature, following Isabelle/fde0b195cb7d; — wenzelm / hgweb
  17. reduced prominence of lemma names — haftmann / hgweb
  18. merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  19. regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  20. sync web abstract — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  21. adapted ROOT file link to afp-2023; — Fabian Huch <huch@in.tum.de> / hgweb
  22. merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  23. web: 2023 downlaod links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  24. Added tag Isabelle2023 for changeset 01bf5fad3e59 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  25. add 2023 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  26. website regen — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  27. fix toml key generated by afp_releases — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  28. set Isabelle2023 release date — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  29. update Isabelle2022 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  30. afp release path has changed on isa-afp.org — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  31. fix afp-submit for markdown processing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  32. Moved a general purpose theorem into the main repository — paulson <lp15@cam.ac.uk> / hgweb
  33. a little fix involving the reformulated version of inclusion/exclusion — paulson <lp15@cam.ac.uk> / hgweb
  34. fixed missing parenthesis in or-ok-lemma — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  35. new bibiten and titlecase on all sections — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  36. avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated operation; — wenzelm / hgweb
  37. replace underscore latex package with formal markup — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  38. merge — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  39. fix latex generation — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  40. Backed out changeset 8eb0a45852dc — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  41. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  42. avoid non-local return; — Fabian Huch <huch@in.tum.de> / hgweb
  43. removed migration tools; — Fabian Huch <huch@in.tum.de> / hgweb
  44. follow naming conventions of Isabelle/2a99fcb283ee; — wenzelm / hgweb
  45. adapted to Isabelle/fd1fec53665b; — wenzelm / hgweb
  46. Relational_Disjoint_Set_Forests: update history — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  47. Relational_Disjoint_Set_Forests: minor text edits — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  48. merged — paulson / hgweb
  49. small fixes — paulson <lp15@cam.ac.uk> / hgweb
  50. fix afp-submit for markdown processing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  51. switch version back to devel after fork — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  52. use default AFP chapter settings — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  53. merge from afp-devel — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  54. update version to 2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  55. update author email (by request) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  56. Tree_Enumeration: Fix errors introduced by renamings in Unidrected_Graph_Theory. — Emin Karayel <me@eminkarayel.de> / hgweb
  57. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  58. sitegen for Fixed_Length_Vector — traytel / hgweb
  59. added syntax bundles and disabled syntax by default — traytel / hgweb
  60. moved abstract to root.tex — traytel / hgweb
  61. made proofs more robust — traytel / hgweb
  62. new entry Fixed_Length_Vector — traytel / hgweb
  63. Fixed the title and author of Ceva in the document — paulson <lp15@cam.ac.uk> / hgweb
  64. sitegen for Ceva — paulson <lp15@cam.ac.uk> / hgweb
  65. new entry Ceva — paulson <lp15@cam.ac.uk> / hgweb
  66. for better output notation — Akihisa Yamada <akihisa.yamada@aist.go.jp> / hgweb
  67. regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  68. fix duplicated key in IEEE_Floating_Point.toml — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  69. Merge changes — cledmonds / hgweb
  70. Renamed incident and order to vincident and gorder due to` compatibility issues. — cledmonds / hgweb
  71. Note recent additions (roundNearestTiesToAway, single NaN value, SMT-LIB translation) in metadata. — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  72. Merged. — Dominique Unruh <unruh@ut.ee> / hgweb
  73. Registers: Fixed some broken proofs. — Dominique Unruh <unruh@ut.ee> / hgweb
  74. redefine substitution of terms as special case of general evaluation of terms — Rene Thiemann <rene.thiemann@uibk.ac.at> / 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`. — Dominique Unruh <unruh@ut.ee> / hgweb
  76. update author info — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / 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. — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / hgweb
  78. metadata formatting — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  79. address metadata warnings — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  80. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  81. remove unused metadata (leaves website unchanged) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  82. new entry Catoids — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  83. remove obsolete (AFP) group from new entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  84. Word_Lib: import new material from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  85. update to isabelle@fd8e1bbc0686 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  86. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  87. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  88. New entry Polygonal_Number_Theorem — nipkow / hgweb
  89. Quantales_Converse metadata — paulson <lp15@cam.ac.uk> / hgweb
  90. new entry Quantales_Converse — paulson <lp15@cam.ac.uk> / hgweb
  91. Fixed the punctuation in the title and abstract — paulson <lp15@cam.ac.uk> / hgweb
  92. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser — paulson <lp15@cam.ac.uk> / hgweb
  93. New entry /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser — paulson <lp15@cam.ac.uk> / hgweb
  94. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  95. tuned links in theory view; — Fabian Huch <huch@in.tum.de> / hgweb
  96. tuned instructions; — Fabian Huch <huch@in.tum.de> / hgweb
  97. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  98. clarify statistics-ignore flag and build example submission properly; — Fabian Huch <huch@in.tum.de> / hgweb
  99. regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  100. rectify copy/paste error — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  101. merged — paulson / hgweb
  102. Redid an ugly proof — paulson <lp15@cam.ac.uk> / hgweb
  103. construction for anchord GTT intersection

    by Alexander Lochman — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  104. merged — paulson / hgweb
  105. Updated the root file to start from an AFP image — paulson <lp15@cam.ac.uk> / hgweb
  106. tuned — nipkow / hgweb
  107. merged — nipkow / hgweb
  108. new editors Lammich and Traytel — nipkow / hgweb
  109. Eliminated needless import and rationalised the ROOT file — paulson <lp15@cam.ac.uk> / hgweb
  110. Deleted needless imports — paulson <lp15@cam.ac.uk> / hgweb
  111. Generalised and tidied an intermediate result — paulson <lp15@cam.ac.uk> / hgweb
  112. Higher_Order_Terms: add fresh_list function — Lars Hupel <lars@hupel.info> / hgweb
  113. delete unneeded file — Lars Hupel <lars@hupel.info> / hgweb
  114. antiquoting special symbols in text — davfuenmayor@gmail.com / hgweb
  115. merge with default — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  116. Relational_Disjoint_Set_Forests: extended theory, refactored related entries — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  117. Refactored and updated entry. Synchronize with companion paper. — davfuenmayor@gmail.com / hgweb
  118. simplified proof without auxiliary function — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  119. provide more unification algorithms, e.g., to compute mgu's modulo variable renamings — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  120. Adapted to devel — nipkow / hgweb
  121. Relational_Disjoint_Set_Forests: simplified invariant — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  122. Bell_Numbers_Spivey: Add code equations for the computation of Bell numbers. — Emin Karayel <me@eminkarayel.de> / 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. — Emin Karayel <me@eminkarayel.de> / hgweb
  124. proved a few properties of WPO with less assumption, so that Co-WPO properties can be derived — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  125. Fixed LaTeX. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  126. Merge. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  127. Fixed missing entries in ROOTS file (previous erronous commit). — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  128. Normalised email. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  129. Improved setup of the symbolic evaluator. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  130. Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / 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. — Emin Karayel <me@eminkarayel.de> / hgweb
  132. merged — paulson / hgweb
  133. Adjustments for recent cosmetic changes to the Distribution — paulson <lp15@cam.ac.uk> / hgweb
  134. Proper epsilon-syntax — paulson <lp15@cam.ac.uk> / hgweb
  135. Merge. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  136. Minor improvement of handling of string literals in symbolic evaluator. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  137. Removing redundant definitions:
    - External
    - Fallback — dmarmsoler / hgweb
  138. tuned — nipkow / hgweb
  139. Merge — dmarmsoler / hgweb
  140. Updating history for Isabelle/Solidity — dmarmsoler / 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. — dmarmsoler / hgweb
  142. Relational_Disjoint_Set_Forests: added a new theory, refactored related entries — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  143. remove some redundant constraint-types in simplex algorithm — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  144. relation between has-maximum and bdd_above — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  145. tuned names — nipkow / hgweb
  146. merged — nipkow / hgweb
  147. more comments — nipkow / hgweb
  148. merged — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  149. back out Paraconsistency — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  150. merged — nipkow / hgweb
  151. tuned and simplified proofs — nipkow / hgweb
  152. Some additions to IICF by Valentin Springsklee — Peter Lammich / hgweb
  153. merge — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  154. small changes in FOL_Seq_Calc1 metadata — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  155. More Paraconsistency — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
  156. merged — wenzelm / hgweb
  157. tuned — nipkow / hgweb
  158. tuned — nipkow / hgweb
  159. prefer existing Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
  160. proper .ML file names; — wenzelm / hgweb
  161. proper .ML file name; — wenzelm / hgweb
  162. eliminated suspicious Unicode character, which often produce unexpected document output; — wenzelm / hgweb
  163. eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
  164. tuned whitespace; — wenzelm / hgweb
  165. avoid hardwired document output; — wenzelm / hgweb
  166. eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
  167. tuned signature; — wenzelm / hgweb
  168. fixed build following a13761ef6796 — desharna / hgweb
  169. merged — desharna / hgweb
  170. removed unnecessary theory with potential for name conflict — desharna / hgweb
  171. provided var2-versions of all doubly-nested loops — nipkow / hgweb
  172. Added version of algorithm 4 with precise variant var2 and tuned — nipkow / hgweb
  173. Floyd Warshall: improve code refinements — Simon Wimmer <wimmers@in.tum.de> / hgweb
  174. IMP2: fix typos — Simon Wimmer <wimmers@in.tum.de> / hgweb
  175. New check 'coverage_rcv' added. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  176. Fixing typos. — Achim D. Brucker <adbrucker@0x5f.org> / 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 — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  178. typos — nipkow / hgweb
  179. remove AFP group already defined by chapter; — Fabian Huch <huch@in.tum.de> / hgweb
  180. Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb

#29 (Jul 13, 2023, 8:33:11 PM)

  1. fix merge problems; — Fabian Huch <huch@in.tum.de> / hgweb

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

  1. merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
  2. re-generate site; — Fabian Huch <huch@in.tum.de> / hgweb
  3. tuned for smaller diffs; — Fabian Huch <huch@in.tum.de> / hgweb
  4. New topic for Gray_Codes — nipkow / hgweb
  5. More Gray_Codes — nipkow / hgweb
  6. More Gray_Codes — nipkow / hgweb
  7. New entry Gray_Codes — nipkow / hgweb
  8. metadata and sitegen for Executable_Randomized_Algorithms — paulson <lp15@cam.ac.uk> / hgweb
  9. New entry Executable_Randomized_Algorithms — paulson <lp15@cam.ac.uk> / hgweb
  10. new entry DCR-ExecutionEquivalence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  11. Zeckendorf: metadata and sitegen — paulson <lp15@cam.ac.uk> / hgweb
  12. new entry Zeckendorf — paulson <lp15@cam.ac.uk> / hgweb
  13. Crypto_Standards: Fixed a spelling error — paulson <lp15@cam.ac.uk> / hgweb
  14. Crypto_Standards metadata & website — paulson <lp15@cam.ac.uk> / hgweb
  15. New entry Crypto_Standards — paulson <lp15@cam.ac.uk> / hgweb
  16. move TOML module to Isabelle (see Isabelle/be8aaaa4ac25); — Fabian Huch <huch@in.tum.de> / hgweb
  17. added missing timeout; — Fabian Huch <huch@in.tum.de> / hgweb
  18. reformat; — Fabian Huch <huch@in.tum.de> / hgweb
  19. remove duplicate fields; — Fabian Huch <huch@in.tum.de> / hgweb
  20. check TOML parse structure properly; — Fabian Huch <huch@in.tum.de> / hgweb
  21. proper typed TOML layer; — Fabian Huch <huch@in.tum.de> / hgweb
  22. tuned imports; — Fabian Huch <huch@in.tum.de> / hgweb
  23. Updated links — nipkow / hgweb
  24. Added citations — nipkow / hgweb
  25. Added citations — nipkow / hgweb
  26. Added citations — nipkow / hgweb
  27. Added refs — nipkow / hgweb
  28. Added DOIs — nipkow / hgweb
  29. Added DOIs — nipkow / hgweb
  30. Added DOIs — nipkow / hgweb
  31. Added DOI — nipkow / hgweb
  32. Added DOI — nipkow / hgweb
  33. added DOI — nipkow / hgweb
  34. Median_Method: Add a tight version of the median bound, suggested by Yong Kiam Tan. — Emin Karayel <me@eminkarayel.de> / hgweb
  35. parse proper toml syntax; — Fabian Huch <huch@in.tum.de> / hgweb
  36. Syntax for symmetric set difference, plus tidying — paulson <lp15@cam.ac.uk> / hgweb
  37. Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
  38. Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
  39. Add — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
  40. Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
  41. Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
  42. merged — paulson / hgweb
  43. Three_Squares: time limit increase; and now sym_diff is declared in main HOL — paulson <lp15@cam.ac.uk> / hgweb
  44. moved Subterm_and_Context into First_Order_Terms, merged context of Term_Aux into Term — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  45. replace scala.sys.process with proper Bash.Process; — Fabian Huch <huch@in.tum.de> / hgweb
  46. renamed "flatten" to "unindex" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  47. Resolved some operator clashes — paulson <lp15@cam.ac.uk> / hgweb
  48. merged — paulson / hgweb
  49. simplified some proofs — paulson <lp15@cam.ac.uk> / hgweb
  50. Modifications for moving from f ` S <= T to f:S->T — paulson <lp15@cam.ac.uk> / hgweb
  51. Updated for new HOL-CSP — Burkhart Wolff <wolff@lri.fr> / hgweb
  52. merge — Burkhart Wolff <wolff@lri.fr> / hgweb
  53. updated ROOT. — Burkhart Wolff <wolff@lri.fr> / hgweb
  54. Registers: Fixed nonterminating subproof — Dominique Unruh <unruh@ut.ee> / 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 — Dominique Unruh <unruh@ut.ee> / hgweb
  56. Renamings of operators, and a major theorem on distributivity of Mprefix vs Sync. Renamings of some lemmata. — Burkhart Wolff <wolff@lri.fr> / 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 — Emin Karayel <me@eminkarayel.de> / hgweb
  58. metadata and sitegen for Directed_Sets — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  59. new entry: Directed_Sets — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  60. merge from AFP 2022 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  61. metadata and sitegen for Multirelations_Heterogeneous — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  62. new entry: Multirelations_Heterogeneous — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  63. adjust Schwartz_Zippel entry

    - Use Pi_pmf from HOL-Probability
    - Generalize theorem(s) in example — Yong Kiam Tan <yongkiat@cs.cmu.edu> / hgweb
  64. adjusted Simple_Clause_Learning from AFP 2022 to AFP devel — desharna / hgweb
  65. adjusted Given_Clause_Loops from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  66. adjusted CommCSL from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  67. adjusted DigitsInBase from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  68. adjusted Schwartz_Zippel from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  69. adjusted TsirelsonBound from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  70. adjusted Tree_Enumeration from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  71. adjusted efficient WPO from AFP 2022 to afp devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  72. merge from afp-2022 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  73. New entry Efficient_Weighted_Path_Order — nipkow / hgweb
  74. add edit mode to afp-submit UI; — Fabian Huch <huch@in.tum.de> / hgweb
  75. solved subtle problem with multiple entries and new authors; — Fabian Huch <huch@in.tum.de> / hgweb
  76. better error logging; — Fabian Huch <huch@in.tum.de> / hgweb
  77. added edit handler to submission app; — Fabian Huch <huch@in.tum.de> / hgweb
  78. added frontend in devel mode; — Fabian Huch <huch@in.tum.de> / hgweb
  79. tuned (mostly api path handling); — Fabian Huch <huch@in.tum.de> / hgweb
  80. A real title in place of MLSS_Decision_Proc — paulson <lp15@cam.ac.uk> / hgweb
  81. MLSS_Decision_Proc sitegen — paulson <lp15@cam.ac.uk> / hgweb
  82. New entry MLSS_Decision_Proc — paulson <lp15@cam.ac.uk> / hgweb
  83. metadata and sitegen for TsirelsonBound — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  84. new entry: TsirelsonBound — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  85. New entry Tree_Enumeration — nipkow / hgweb
  86. Three_Squares citegen — paulson <lp15@cam.ac.uk> / hgweb
  87. New entry Three_Squares — paulson <lp15@cam.ac.uk> / hgweb
  88. fixed some ACM/AMS categories — Manuel Eberl <manuel@pruvisto.org> / hgweb
  89. more files — nipkow / hgweb
  90. New entry MHComputation — nipkow / hgweb
  91. make index.json files line-by-line for smaller diffs; — Fabian Huch <huch@in.tum.de> / hgweb
  92. cleanup; — Fabian Huch <huch@in.tum.de> / hgweb
  93. added new entry DigitsInBase; — Fabian Huch <huch@in.tum.de> / hgweb
  94. fixed broken LaTeX quotation marks in abstracts — Manuel Eberl <eberlm@in.tum.de> / hgweb
  95. recategorised some entries — Manuel Eberl <eberlm@in.tum.de> / hgweb
  96. new topic: Computer science/Algorithms/Randomized — Manuel Eberl <eberlm@in.tum.de> / hgweb
  97. sitegen for Schwartz_Zippel — Manuel Eberl <manuel@pruvisto.org> / hgweb
  98. new entry: Schwartz_Zippel — Manuel Eberl <manuel@pruvisto.org> / hgweb
  99. New entry: Simple_Clause_Learning — nipkow / hgweb
  100. New entry HyperHoareLogic — nipkow / hgweb
  101. New entry Distributed_Distinct_Elements — nipkow / hgweb
  102. metadata for CommCSL + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  103. new entry: CommCSL — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  104. New entry No_FTL_observers_Gen_Rel — nipkow / hgweb
  105. added new files generated by sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  106. sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  107. metadata for Expander Graphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  108. new entry: Expander Graphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  109. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  110. fix of toml-entries and rerun of sitegen: problem: links where in these quotes: ”...” and not in the standard ones "..." — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  111. sitegen (for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  112. metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  113. new entry: Two_Generated_Word_Monoids_Intersection — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  114. new entry: Binary_Code_Imprimitive — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  115. running sort on ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  116. New entry Probability_Inequality_Completeness — nipkow / hgweb
  117. Rensets metadata — paulson / hgweb
  118. New entry Rensets — paulson <lp15@cam.ac.uk> / hgweb
  119. more Edwards — nipkow / hgweb
  120. New entry Edwards_Elliptic_Curves_Group — nipkow / hgweb
  121. metadata and sitegen for CVP_Hardness — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  122. new entry: CVP_Hardness — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  123. rerun sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  124. revert proof compression experiment — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  125. metadata for ABY3_Protocols — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  126. new entry ABY3_Protocols — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  127. sitegen for Given_Clause_Loops — paulson <lp15@cam.ac.uk> / hgweb
  128. New entry Given_Clause_Loops — paulson <lp15@cam.ac.uk> / hgweb
  129. Adjustments for the simplified version of real_le_lsqrt — paulson <lp15@cam.ac.uk> / hgweb
  130. adapted to Isabelle/84a7a0029c82 — desharna / hgweb
  131. merged — desharna / hgweb
  132. adapted to Isabelle/0252d635bfb2 — desharna / hgweb
  133. merge — Burkhart Wolff <wolff@lri.fr> / hgweb
  134. merge — Burkhart Wolff <wolff@lri.fr> / hgweb
  135. Merge with developper version on LISN gut — Burkhart Wolff <wolff@lri.fr> / hgweb
  136. merged — wenzelm / hgweb
  137. prefer @{attributes} antiquotation over Attrib.internal;
    adapted to Isabelle/bc42c074e58f; — wenzelm / hgweb
  138. tuned proofs; — wenzelm / hgweb
  139. Deleted a superfluous assumption. This proof is a horror — paulson <lp15@cam.ac.uk> / hgweb
  140. merged — paulson / hgweb
  141. fixed some bibliographic entries — paulson <lp15@cam.ac.uk> / hgweb
  142. merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  143. tuned — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  144. merged — wenzelm / hgweb
  145. merged — wenzelm / hgweb
  146. adapted to current Isabelle/ec1c0daa3fbd; — wenzelm / hgweb
  147. adapted to current Isabelle/ec1c0daa3fbd; — wenzelm / hgweb
  148. adapted to Isabelle/5edd5b12017d; — wenzelm / hgweb
  149. proper morphism context; — wenzelm / hgweb
  150. backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531; — wenzelm / hgweb
  151. proper morphism context; — wenzelm / hgweb
  152. adapted to Isabelle/5ab5add88922; — wenzelm / hgweb
  153. SMT-LIB interpretation of floating-point arithmetic — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  154. merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  155. SMT-LIB interpretation of floating-point arithmetic — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  156. IEEE model with a single NaN value — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  157. Minor — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  158. merging — JeremyDubut <dubutjeremy@gmail.com> / hgweb
  159. updates for future formalizations — JeremyDubut <dubutjeremy@gmail.com> / hgweb
  160. adapted to Isabelle/f78cdc6fe971; — wenzelm / hgweb
  161. adapted to Isabelle/f78cdc6fe971; — wenzelm / hgweb
  162. A slight beautification — paulson <lp15@cam.ac.uk> / hgweb
  163. adapted to 3f354d5bbf98; — wenzelm / hgweb
  164. Rounding modes renamed — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  165. merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  166. Add the rounding mode roundNearestTiesToAway. — Tjark Weber <tjark.weber@it.uu.se> / hgweb
  167. Merge realtime deque renamings — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  168. simplify some measurements — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  169. rename Deque.Idle to Idles — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  170. Rename Big and Small cases — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  171. rename `Transforming` to `Rebal` — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  172. rename `Common.state` to `common_state` — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  173. rename Small.state to small_state — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  174. rename Big.state to big_state — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  175. backed out changeset 2ecb8f5e085f: obsolete thanks to Isabelle/21cdcd120a78; — wenzelm / hgweb
  176. more robust: make it work with Isabelle/a12c48fbf10f; — wenzelm / hgweb
  177. adapted to Isabelle/c4677a6aae2c; — wenzelm / hgweb
  178. adapted to Isabelle/c4677a6aae2c; — wenzelm / hgweb

#27 (May 5, 2023, 10:30:08 AM)

  1. modificaiton due to latex — nanjiang <nanjiang@whu.edu.cn> / hgweb
  2. some small modifications — nanjiang <nanjiang@whu.edu.cn> / hgweb

#26 (May 4, 2023, 2:11:51 PM)

  1. merged — Fabian Huch <huch@in.tum.de> / hgweb
  2. Some hyphens that should be en dashes — paulson <lp15@cam.ac.uk> / hgweb
  3. slightly refine WPO-definition
    - previous formalization of WPO deviated a bit to paper version (requiring less computation)
    - both versions are equivalent whenever order in parameter is strongly normalizing
    - however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders
    - consequence: change formalization so that it is more closely related to paper version,
      so that also results on coWPO can be proven — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  4. merged — wenzelm / hgweb
  5. no "open" of ML structures: it makes sources unmaintainable; — wenzelm / hgweb
  6. adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
  7. adapted to Isabelle/f4cd6e3b5075; — wenzelm / hgweb
  8. adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
  9. This file should have been removed in the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  10. Sync with my development repo.  Main changes related to CartesianMonoidalCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  11. update timing; — wenzelm / hgweb
  12. eliminated pointless parallelism: approx. 1.3s as plain sequential ML; — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp; — wenzelm / hgweb
  15. adapted to Isabelle/c274f52b11ff; — wenzelm / hgweb
  16. Backed out changeset a537fb4c92af — wenzelm / hgweb
  17. slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d; — wenzelm / hgweb
  18. merged — nipkow / hgweb
  19. moved lemma to FDS exercises — nipkow / hgweb
  20. Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
  21. Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad

    The rule is necessary for the termination proof of some recursive functions
    over the time monad. — Emin Karayel <me@eminkarayel.de> / hgweb
  22. tuned; — wenzelm / hgweb
  23. tuned; — wenzelm / hgweb
  24. eliminated aliases: prefer existing Thm.elim_implies; — wenzelm / hgweb
  25. tuned; — wenzelm / hgweb
  26. more standard use of structure Unsynchronized; — wenzelm / hgweb
  27. tuned whitespace; — wenzelm / hgweb
  28. not unused! — nipkow / hgweb
  29. Added running time analysis — nipkow / hgweb
  30. some remarks on division — haftmann / hgweb
  31. clarified scope of document — haftmann / hgweb
  32. no subsection without section — haftmann / hgweb
  33. merged — paulson / hgweb
  34. Deleted library material — paulson <lp15@cam.ac.uk> / hgweb
  35. adapted to Isabelle/b43ee37926a9; — wenzelm / hgweb
  36. merged — wenzelm / hgweb
  37. adapted to Isabelle/13cee8c2ed8d; — wenzelm / hgweb
  38. Add related entry for Combinatorial_Enumeration_Algorithms.

    Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references
    Note: Ran sitegen. — Emin Karayel <me@eminkarayel.de> / hgweb
  39. small simplifications — blanchet / hgweb
  40. shortened some parts of Huffman proof using Sledgehammer — blanchet / hgweb
  41. added another simplification rule when alternatives are equal — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  42. added more simplification rules involving Zero — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  43. adapted to Isabelle/4a174bea55e2; — wenzelm / hgweb
  44. uodated map update syntax — nipkow / hgweb
  45. Adjusted to changes in distribution. — haftmann / hgweb
  46. more realistic timeout; — wenzelm / hgweb
  47. avoid hardwired documents;
    tuned whitespace; — wenzelm / hgweb
  48. merged — paulson / hgweb
  49. simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  50. added character sets to the extension directory of regular expressions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  51. more syntax adjustments — nipkow / hgweb
  52. more syntax update for map update syntax — nipkow / hgweb
  53. more map update syntax updates — nipkow / hgweb
  54. merged — nipkow / hgweb
  55. updated to new map update syntax priorities — nipkow / hgweb
  56. Some simplifications of proofs — paulson <lp15@cam.ac.uk> / hgweb
  57. Minor refinements — paulson <lp15@cam.ac.uk> / hgweb
  58. tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
  59. tidied another file — paulson <lp15@cam.ac.uk> / hgweb
  60. tidied a bit more — paulson <lp15@cam.ac.uk> / hgweb
  61. merged — paulson / hgweb
  62. More tidying — paulson <lp15@cam.ac.uk> / hgweb
  63. completed the addtion of Rec in the Extension directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  64. added another regular expression for Record — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  65. More tidying of the Ordinal entry — paulson <lp15@cam.ac.uk> / hgweb
  66. A massive tidying — paulson <lp15@cam.ac.uk> / hgweb
  67. Tiny bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
  68. more robust: allow optional arguments in isabelle.Progress.echo; — wenzelm / hgweb
  69. More tidying — paulson <lp15@cam.ac.uk> / hgweb
  70. merged — paulson / hgweb
  71. Suppression of duplicate syntax for abs_summable_on, etc. — paulson <lp15@cam.ac.uk> / hgweb
  72. No more sorted_take, sorted_drop — paulson <lp15@cam.ac.uk> / hgweb
  73. Update entries MDP-Rewards and MDP-Algorithms — Maximilian Schaeffeler <maximilian.schaeffeler@tum.de> / hgweb
  74. Migration of material from Jordan_Hoelder to HOL-Algebra — paulson <lp15@cam.ac.uk> / hgweb
  75. merged — paulson / hgweb
  76. Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  77. Adjustments for the new infix status of has_sum — paulson <lp15@cam.ac.uk> / hgweb
  78. A tiny spelling correction — paulson <lp15@cam.ac.uk> / hgweb
  79. merged — paulson / hgweb
  80. A little more migration — paulson <lp15@cam.ac.uk> / hgweb
  81. Backed out changeset fa59c080cb3b — nipkow / hgweb
  82. Backed out changeset 811f0b8d4f58 — nipkow / hgweb
  83. tuned metis call to avoid obscure feature — blanchet / hgweb
  84. merged — paulson / hgweb
  85. Migration of material to the repository and necessary modifications — paulson <lp15@cam.ac.uk> / hgweb
  86. more map_of adaptions — nipkow / hgweb
  87. adapted to new List.map_of — nipkow / hgweb
  88. update Real_Time_Deque — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  89. Removal of a stray sledgehammer command — paulson <lp15@cam.ac.uk> / hgweb
  90. explicit range types in abstractions — stuebinm <stuebinm@disroot.org> / hgweb
  91. somehow more clear terminology — haftmann / hgweb
  92. merged — paulson / hgweb
  93. Some tidying and moving some material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
  94. Deleted use of Euclidean_Division — Katharina Kreuzer / hgweb
  95. Repaired session name — Katharina Kreuzer / hgweb
  96. "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium" — Katharina Kreuzer / hgweb
  97. Update names to match thesis. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  98. proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions; — wenzelm / hgweb
  99. proper symbolic handle on component resources (see Isabelle/3eb3de867786); — wenzelm / hgweb
  100. more realistic timeout, based on CPU time; — wenzelm / hgweb
  101. adapted to Isabelle/9a60c1759543; — wenzelm / hgweb
  102. more realistic timeout, based on CPU time; — wenzelm / hgweb
  103. fixed looping proofs — paulson <lp15@cam.ac.uk> / hgweb
  104. dropped reference to dead clone — haftmann / hgweb
  105. removed dead clone — haftmann / hgweb
  106. modernized — haftmann / hgweb
  107. Modernized. — haftmann / hgweb
  108. More instances. — haftmann / hgweb
  109. Tuned whitespace. — haftmann / hgweb
  110. Updated references. — haftmann / hgweb
  111. More correct references. — haftmann / hgweb
  112. Removed a bit of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
  113. merged — paulson / hgweb
  114. Shortened several messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  115. Fix name clash in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
  116. Fixed a name clash — paulson <lp15@cam.ac.uk> / hgweb
  117. Moving more material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
  118. Moving some material to the main repository — paulson <lp15@cam.ac.uk> / hgweb
  119. adapted to db93f67a; — Fabian Huch <huch@in.tum.de> / hgweb
  120. merged — Fabian Huch <huch@in.tum.de> / hgweb
  121. generalized theory name: euclidean division denotes one particular division definition on integers — haftmann / hgweb
  122. more efficient specification — haftmann / hgweb
  123. merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
  124. metadata for Suppes' theorem + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  125. new entry: Suppes' Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  126. new entry HoareForDivergence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  127. tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
  128. metadat for StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  129. new entry StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  130. tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
  131. cleanup accidental unused document files; — Fabian Huch <huch@in.tum.de> / hgweb
  132. check ROOTs: add warning-only checks; — Fabian Huch <huch@in.tum.de> / hgweb
  133. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  134. add ROOT checks for document presence and unused files; — Fabian Huch <huch@in.tum.de> / hgweb
  135. afp-submit visual improvements; — Fabian Huch <huch@in.tum.de> / hgweb
  136. update bibtex example; — Fabian Huch <huch@in.tum.de> / hgweb
  137. new doi — nipkow / hgweb
  138. sitegen for AOT — paulson <lp15@cam.ac.uk> / hgweb
  139. merged — paulson / hgweb
  140. New entry AOT — paulson <lp15@cam.ac.uk> / hgweb
  141. New entry: Propositional_Logic_Class — nipkow / hgweb
  142. sitegen for Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
  143. New entry Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
  144. Sorry — extra files for Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  145. Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  146. New entry Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  147. New entry: Synthetic_Completeness — nipkow / hgweb
  148. New entry: Quantifier_Elimination_Hybrid — nipkow / hgweb
  149. New entry Birkhoff_Finite_Distributive_Lattices — nipkow / hgweb
  150. sitegen for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  151. metadata for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  152. new entry: Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  153. sitegen for Turan — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  154. added metadata for Turans graph theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  155. new entry: Turans Graph Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  156. new entry Multitape_To_Singletape_TM — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  157. removed static pages from rss feed; — Fabian Huch <huch@in.tum.de> / hgweb
  158. Minor rerating of the abstract of Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  159. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  160. New entry Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  161. sitegen for the aforementioned changes — paulson <lp15@cam.ac.uk> / hgweb
  162. adjustments to the abstract, requested by the author — paulson <lp15@cam.ac.uk> / hgweb
  163. CHERI-C_Memory_Model patch & metadata — paulson <lp15@cam.ac.uk> / hgweb
  164. New submission CHERI-C_Memory_Model — paulson <lp15@cam.ac.uk> / hgweb
  165. updated docs; — Fabian Huch <huch@in.tum.de> / hgweb
  166. improve page layout slightly; — Fabian Huch <huch@in.tum.de> / hgweb
  167. fixed broken abstract for PAPP_Impossibility — Manuel Eberl <manuel@pruvisto.org> / hgweb
  168. remove dead code — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  169. metadata and sitegen for PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  170. new entry PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  171. remove old .sitegen-ignore and mention AFP chapter in submission guidelines; — Fabian Huch <huch@in.tum.de> / hgweb
  172. afp_check_roots: proper error message printing; — Fabian Huch <huch@in.tum.de> / hgweb
  173. metadata and sitegen for Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  174. new entry: Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  175. tuned check names; — Fabian Huch <huch@in.tum.de> / hgweb
  176. make check roots tool less dependent on AFP structure; — Fabian Huch <huch@in.tum.de> / hgweb
  177. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  178. web for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  179. sitegen for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  180. New entry Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  181. fix duplicate affiliations from author and notify; — Fabian Huch <huch@in.tum.de> / hgweb
  182. add metadata check tool to sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  183. update check tools: add formatting checks, new cmd options; — Fabian Huch <huch@in.tum.de> / hgweb
  184. check for entries instead of session due to session nesting allowed in entries; — Fabian Huch <huch@in.tum.de> / hgweb
  185. added unused thy check; — Fabian Huch <huch@in.tum.de> / hgweb
  186. clarified check roots tool; — Fabian Huch <huch@in.tum.de> / hgweb
  187. afp-submit: tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
  188. afp-submit: encode new notify addresses properly; — Fabian Huch <huch@in.tum.de> / hgweb
  189. afp-submit: correct build status on empty file; — Fabian Huch <huch@in.tum.de> / hgweb
  190. afp-submit: remove padding on select; — Fabian Huch <huch@in.tum.de> / hgweb
  191. re-format metadata; — Fabian Huch <huch@in.tum.de> / hgweb
  192. afp-submit: update on correct status change; — Fabian Huch <huch@in.tum.de> / hgweb
  193. afp-submit: clarified date format, tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
  194. switch fonts to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
  195. switch to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
  196. clarified afp-submit error handling; — Fabian Huch <huch@in.tum.de> / hgweb
  197. clarified afp-submit creation and message; — Fabian Huch <huch@in.tum.de> / hgweb
  198. list submission system website; — Fabian Huch <huch@in.tum.de> / hgweb
  199. afp-submit: clarified api urls; — Fabian Huch <huch@in.tum.de> / hgweb
  200. Removal of more unused material — paulson <lp15@cam.ac.uk> / hgweb
  201. Small simplifications. Removed a needless assumption. — paulson <lp15@cam.ac.uk> / hgweb
  202. isabelle update -u cite; — wenzelm / hgweb
  203. more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc; — wenzelm / hgweb
  204. Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author) — paulson <lp15@cam.ac.uk> / hgweb
  205. merged — paulson / hgweb
  206. Added the missing .bib file — paulson <lp15@cam.ac.uk> / hgweb
  207. proper bib context for formal citations, although there is no document; — wenzelm / hgweb
  208. back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
  209. back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
  210. back to unchecked \cite: there is entry lacks .bib file; — wenzelm / hgweb
  211. proper citation; — wenzelm / hgweb
  212. merged — desharna / hgweb
  213. added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp] — desharna / hgweb
  214. merged — wenzelm / hgweb
  215. isabelle update -u cite; — wenzelm / hgweb
  216. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
  217. consistent casing in \cite — Lars Hupel <lars.hupel@mytum.de> / hgweb
  218. ETTS: updated bibliography and citations — user9716869 <user9716869@gmail.com> / hgweb
  219. merged — wenzelm / hgweb
  220. more correct and complete citations; — wenzelm / hgweb
  221. unchecked \cite for unidentifiable citation; — wenzelm / hgweb
  222. proper @{cite} syntax; — wenzelm / hgweb
  223. isabelle update -u cite; — wenzelm / hgweb
  224. Updating Risk Free Lending Entry

      - Adding lemma for transfers in special case
      - Fixing grammar in abstract
      - Adding citation — Matthew Doty <matt@w-d.org> / hgweb
  225. added bibliography to ROOT; — Fabian Huch <huch@in.tum.de> / hgweb
  226. CTR and ETTS: several amendments (fact names, printing, presentation) — user9716869 <user9716869@gmail.com> / hgweb
  227. Removed a reference to the (redundant) wf_restr — paulson <lp15@cam.ac.uk> / hgweb
  228. added bibliographies to ROOTs; — Fabian Huch <huch@in.tum.de> / hgweb
  229. Changes for generalised lemmas — Katharina Kreuzer / hgweb
  230. Changes for generalised lemmas — Katharina Kreuzer / hgweb
  231. Generalised Lemmas — Katharina Kreuzer / hgweb
  232. merged — desharna / hgweb
  233. adapted to Isabelle/c9e091867206 — desharna / hgweb
  234. tuned; — wenzelm / hgweb
  235. tuned signature, following Isabelle/947510ce4e36; — wenzelm / hgweb
  236. adapted to Isabelle/25900fbea7ad;
    fewer clones of Isabelle sources; — wenzelm / hgweb
  237. adapted to Isabelle/b61ad889dffa — desharna / hgweb
  238. removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL — desharna / hgweb
  239. merged — desharna / hgweb
  240. adapted to Isabelle/d33fc5228aae — desharna / hgweb
  241. fixed proof following Isabelle/66cae055ac7b — desharna / hgweb
  242. merge — blanchet / hgweb
  243. adapted to Isabelle/c48fe2be847f — blanchet / hgweb
  244. enable -no-pie for CakeML — Lars Hupel <lars.hupel@mytum.de> / hgweb
  245. fixed proofs and removed duplicates following Isabelle/e65a50f6c2de — desharna / hgweb
  246. tuned proofs to use asymI, asymD, asympI, and asympD — desharna / hgweb
  247. Fix failing continuous integration — desharna / hgweb
  248. fixed proof following Isabelle/8fff4e4d81cb — desharna / hgweb
  249. removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL — desharna / hgweb
  250. added lemma imgu_range_vars_subset — desharna / hgweb
  251. Update headers and metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  252. Fix ROOT again — Asta Halkjær From <andro.from@gmail.com> / hgweb
  253. Fix ROOT — Asta Halkjær From <andro.from@gmail.com> / hgweb
  254. Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  255. Fixed proofs following Isabelle/a7d2a7a737b8 — desharna / hgweb
  256. added lemmas mem_range_varsI and imgu_subst_domain_subset — desharna / hgweb
  257. weakened the definition of redundant_inference — desharna / hgweb
  258. removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL — desharna / hgweb
  259. fixed Containers following introduction of irrefl_on — desharna / hgweb
  260. added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset — desharna / hgweb
  261. name change — nipkow / hgweb
  262. AFP and DBLP — nipkow / hgweb
  263. merged — desharna / hgweb
  264. added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset — desharna / hgweb
  265. added lemma subst_domain_rename_subst_domain_subset — desharna / hgweb
  266. added lemma image_the_Var_image_subst_renaming_eq — desharna / hgweb
  267. Added acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
  268. Added code export to ROOT — mohammadabdulaziz / hgweb
  269. Removed out of place code — mohammadabdulaziz / hgweb
  270. tuned lemma subst_domain_restrict_subst_domain — desharna / hgweb
  271. added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp] — desharna / hgweb
  272. added attribute [simp] to lemma rename_subst_domain_Var_rhs — desharna / hgweb
  273. added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp] — desharna / hgweb
  274. merged — desharna / hgweb
  275. removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL — desharna / hgweb
  276. removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL — desharna / hgweb
  277. added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp] — desharna / hgweb
  278. added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset — desharna / hgweb
  279. Streamlined a proof — paulson <lp15@cam.ac.uk> / hgweb
  280. added lemmas — desharna / hgweb
  281. moved lemma around — desharna / hgweb
  282. redefined mgu as a definition — desharna / hgweb
  283. tuned naming — desharna / hgweb
  284. fixed proof — desharna / hgweb
  285. added definition restrict_subst_domain and associated lemmas — desharna / hgweb
  286. tuned (sub)subsection — desharna / hgweb
  287. added lemma member_image_the_Var_image_subst — desharna / hgweb
  288. added lemmas unify_subst_domain_range_vars_disjoint — desharna / hgweb
  289. added lemma unify_range_vars — desharna / hgweb
  290. added lemma unify_subst_domain — desharna / hgweb
  291. added definition rename_subst_domain_range and related lemmas — desharna / hgweb
  292. merged — desharna / hgweb
  293. added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset — desharna / hgweb
  294. Fixed the ROOT file, so that the theory of cardinals is loaded — paulson <lp15@cam.ac.uk> / hgweb
  295. added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term — desharna / hgweb
  296. added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same — desharna / hgweb
  297. added lemma decompose_same_Fun[simp] — desharna / hgweb
  298. added lemma zip_option_same[simp] — desharna / hgweb
  299. added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain — desharna / hgweb
  300. removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
  301. used rho for renamming — desharna / hgweb
  302. tuned assumptions — desharna / hgweb
  303. added lemma subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
  304. added lemmas inv_renaming_sound and ex_inverse_of_renaming — desharna / hgweb
  305. added lemma subst_apply_term_ident — desharna / hgweb
  306. added lemmas subst_range_Var and range_vars_Var and moved stuff around — desharna / hgweb
  307. added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming — desharna / hgweb
  308. tuned naming — desharna / hgweb
  309. added lemma mgu_range_vars — desharna / hgweb
  310. added lemma subst_compose_apply_eq_apply_lhs_if — desharna / hgweb
  311. added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu — desharna / hgweb
  312. RealTimeDeque: replace `reverseN` with `take_rev — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  313. replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on — desharna / hgweb
  314. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  315. add missing thy files in Sturm_Tarski + repair — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  316. afp-submit: style page, improve elements; — Fabian Huch <huch@in.tum.de> / hgweb
  317. afp-submit: added repository updates; — Fabian Huch <huch@in.tum.de> / hgweb
  318. afp-submit: added download and faster file handling; — Fabian Huch <huch@in.tum.de> / hgweb
  319. add submission pages to web ui; — Fabian Huch <huch@in.tum.de> / hgweb
  320. afp-submit: add submission and build status with adapter to existing system; — Fabian Huch <huch@in.tum.de> / hgweb
  321. add user-facing exception handling to web app; — Fabian Huch <huch@in.tum.de> / hgweb
  322. clarified submission handling; — Fabian Huch <huch@in.tum.de> / hgweb
  323. afp-submit: added submission read-only and list views; — Fabian Huch <huch@in.tum.de> / hgweb
  324. add afp-submit web app; — Fabian Huch <huch@in.tum.de> / hgweb
  325. add web app facilities; — Fabian Huch <huch@in.tum.de> / hgweb
  326. RealTimeDeque: Separate implementation and auxiliary functions — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  327. Backed out changeset 3a67df508397
    The finite simproc is no longer active by default — nipkow / hgweb
  328. adapted to new simproc finite — nipkow / hgweb
  329. clarified signature, following Isabelle/f362975e8ba1; — wenzelm / hgweb
  330. more direct Proof_Context.init_global; — wenzelm / hgweb
  331. proper naming conventions for Isabelle/ML; — wenzelm / hgweb
  332. Updated citation — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  333. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  334. Isabelle2022: new release download links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  335. Added tag Isabelle2022 for changeset 548e384c0445 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  336. Removal of some old junk — paulson <lp15@cam.ac.uk> / hgweb
  337. Deleted unused material — paulson <lp15@cam.ac.uk> / hgweb
  338. nothing — paulson <lp15@cam.ac.uk> / hgweb
  339. Instantiation of the order solver for ⊑ and ⊏ (no real effect though) — paulson <lp15@cam.ac.uk> / hgweb
  340. proof simplifications — paulson <lp15@cam.ac.uk> / hgweb
  341. merged — paulson / hgweb
  342. Simplified the proofs a bit — paulson <lp15@cam.ac.uk> / hgweb
  343. merged — desharna / hgweb
  344. replaced fmember.rep_eq by fmember_iff_member_fset — desharna / hgweb
  345. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  346. adapted to Isabelle/457f1cba78fb — desharna / hgweb
  347. merged — desharna / hgweb
  348. added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;
    added simp annotation to generalizes_refl — desharna / hgweb
  349. extracted proof cases from lifting_lemma to distinct lemmas — desharna / hgweb
  350. tuned proof due to new simp rules — nipkow / hgweb
  351. corresponding lemma was removed from distribution — nipkow / hgweb

#24 (May 4, 2023, 1:57:09 PM)

  1. some small modifications — nanjiang <nanjiang@whu.edu.cn> / hgweb

#23 (May 3, 2023, 11:21:29 AM)

  1. Some hyphens that should be en dashes — paulson <lp15@cam.ac.uk> / hgweb
  2. slightly refine WPO-definition
    - previous formalization of WPO deviated a bit to paper version (requiring less computation)
    - both versions are equivalent whenever order in parameter is strongly normalizing
    - however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders
    - consequence: change formalization so that it is more closely related to paper version,
      so that also results on coWPO can be proven — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  3. merged — wenzelm / hgweb
  4. no "open" of ML structures: it makes sources unmaintainable; — wenzelm / hgweb
  5. adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
  6. adapted to Isabelle/f4cd6e3b5075; — wenzelm / hgweb
  7. adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
  8. This file should have been removed in the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  9. Sync with my development repo.  Main changes related to CartesianMonoidalCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  10. update timing; — wenzelm / hgweb
  11. eliminated pointless parallelism: approx. 1.3s as plain sequential ML; — wenzelm / hgweb
  12. tuned; — wenzelm / hgweb
  13. alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp; — wenzelm / hgweb
  14. adapted to Isabelle/c274f52b11ff; — wenzelm / hgweb
  15. Backed out changeset a537fb4c92af — wenzelm / hgweb
  16. slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d; — wenzelm / hgweb
  17. merged — nipkow / hgweb
  18. moved lemma to FDS exercises — nipkow / hgweb
  19. Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
  20. Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad

    The rule is necessary for the termination proof of some recursive functions
    over the time monad. — Emin Karayel <me@eminkarayel.de> / hgweb
  21. tuned; — wenzelm / hgweb
  22. tuned; — wenzelm / hgweb
  23. eliminated aliases: prefer existing Thm.elim_implies; — wenzelm / hgweb
  24. tuned; — wenzelm / hgweb
  25. more standard use of structure Unsynchronized; — wenzelm / hgweb
  26. tuned whitespace; — wenzelm / hgweb
  27. not unused! — nipkow / hgweb
  28. Added running time analysis — nipkow / hgweb
  29. some remarks on division — haftmann / hgweb
  30. clarified scope of document — haftmann / hgweb
  31. no subsection without section — haftmann / hgweb
  32. merged — paulson / hgweb
  33. Deleted library material — paulson <lp15@cam.ac.uk> / hgweb
  34. adapted to Isabelle/b43ee37926a9; — wenzelm / hgweb
  35. merged — wenzelm / hgweb
  36. adapted to Isabelle/13cee8c2ed8d; — wenzelm / hgweb
  37. Add related entry for Combinatorial_Enumeration_Algorithms.

    Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references
    Note: Ran sitegen. — Emin Karayel <me@eminkarayel.de> / hgweb
  38. small simplifications — blanchet / hgweb
  39. shortened some parts of Huffman proof using Sledgehammer — blanchet / hgweb
  40. added another simplification rule when alternatives are equal — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  41. added more simplification rules involving Zero — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  42. adapted to Isabelle/4a174bea55e2; — wenzelm / hgweb
  43. uodated map update syntax — nipkow / hgweb
  44. Adjusted to changes in distribution. — haftmann / hgweb
  45. more realistic timeout; — wenzelm / hgweb
  46. avoid hardwired documents;
    tuned whitespace; — wenzelm / hgweb
  47. merged — paulson / hgweb
  48. simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  49. added character sets to the extension directory of regular expressions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  50. more syntax adjustments — nipkow / hgweb
  51. more syntax update for map update syntax — nipkow / hgweb
  52. more map update syntax updates — nipkow / hgweb
  53. merged — nipkow / hgweb
  54. updated to new map update syntax priorities — nipkow / hgweb
  55. Some simplifications of proofs — paulson <lp15@cam.ac.uk> / hgweb
  56. Minor refinements — paulson <lp15@cam.ac.uk> / hgweb
  57. tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
  58. tidied another file — paulson <lp15@cam.ac.uk> / hgweb
  59. tidied a bit more — paulson <lp15@cam.ac.uk> / hgweb
  60. merged — paulson / hgweb
  61. More tidying — paulson <lp15@cam.ac.uk> / hgweb
  62. completed the addtion of Rec in the Extension directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  63. added another regular expression for Record — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  64. More tidying of the Ordinal entry — paulson <lp15@cam.ac.uk> / hgweb
  65. A massive tidying — paulson <lp15@cam.ac.uk> / hgweb
  66. Tiny bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
  67. more robust: allow optional arguments in isabelle.Progress.echo; — wenzelm / hgweb
  68. More tidying — paulson <lp15@cam.ac.uk> / hgweb
  69. merged — paulson / hgweb
  70. Suppression of duplicate syntax for abs_summable_on, etc. — paulson <lp15@cam.ac.uk> / hgweb
  71. No more sorted_take, sorted_drop — paulson <lp15@cam.ac.uk> / hgweb
  72. Update entries MDP-Rewards and MDP-Algorithms — Maximilian Schaeffeler <maximilian.schaeffeler@tum.de> / hgweb
  73. Migration of material from Jordan_Hoelder to HOL-Algebra — paulson <lp15@cam.ac.uk> / hgweb
  74. merged — paulson / hgweb
  75. Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  76. Adjustments for the new infix status of has_sum — paulson <lp15@cam.ac.uk> / hgweb
  77. A tiny spelling correction — paulson <lp15@cam.ac.uk> / hgweb
  78. merged — paulson / hgweb
  79. A little more migration — paulson <lp15@cam.ac.uk> / hgweb
  80. Backed out changeset fa59c080cb3b — nipkow / hgweb
  81. Backed out changeset 811f0b8d4f58 — nipkow / hgweb
  82. tuned metis call to avoid obscure feature — blanchet / hgweb
  83. merged — paulson / hgweb
  84. Migration of material to the repository and necessary modifications — paulson <lp15@cam.ac.uk> / hgweb
  85. more map_of adaptions — nipkow / hgweb
  86. adapted to new List.map_of — nipkow / hgweb
  87. update Real_Time_Deque — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  88. Removal of a stray sledgehammer command — paulson <lp15@cam.ac.uk> / hgweb
  89. explicit range types in abstractions — stuebinm <stuebinm@disroot.org> / hgweb
  90. somehow more clear terminology — haftmann / hgweb
  91. merged — paulson / hgweb
  92. Some tidying and moving some material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
  93. Deleted use of Euclidean_Division — Katharina Kreuzer / hgweb
  94. Repaired session name — Katharina Kreuzer / hgweb
  95. "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium" — Katharina Kreuzer / hgweb
  96. Update names to match thesis. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  97. proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions; — wenzelm / hgweb
  98. proper symbolic handle on component resources (see Isabelle/3eb3de867786); — wenzelm / hgweb
  99. more realistic timeout, based on CPU time; — wenzelm / hgweb
  100. adapted to Isabelle/9a60c1759543; — wenzelm / hgweb
  101. more realistic timeout, based on CPU time; — wenzelm / hgweb
  102. fixed looping proofs — paulson <lp15@cam.ac.uk> / hgweb
  103. dropped reference to dead clone — haftmann / hgweb
  104. removed dead clone — haftmann / hgweb
  105. modernized — haftmann / hgweb
  106. Modernized. — haftmann / hgweb
  107. More instances. — haftmann / hgweb
  108. Tuned whitespace. — haftmann / hgweb
  109. Updated references. — haftmann / hgweb
  110. More correct references. — haftmann / hgweb
  111. Removed a bit of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
  112. merged — paulson / hgweb
  113. Shortened several messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  114. Fix name clash in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
  115. Fixed a name clash — paulson <lp15@cam.ac.uk> / hgweb
  116. Moving more material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
  117. Moving some material to the main repository — paulson <lp15@cam.ac.uk> / hgweb
  118. adapted to db93f67a; — Fabian Huch <huch@in.tum.de> / hgweb
  119. merged — Fabian Huch <huch@in.tum.de> / hgweb
  120. generalized theory name: euclidean division denotes one particular division definition on integers — haftmann / hgweb
  121. more efficient specification — haftmann / hgweb
  122. merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
  123. metadata for Suppes' theorem + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  124. new entry: Suppes' Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  125. new entry HoareForDivergence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  126. tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
  127. metadat for StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  128. new entry StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  129. tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
  130. cleanup accidental unused document files; — Fabian Huch <huch@in.tum.de> / hgweb
  131. check ROOTs: add warning-only checks; — Fabian Huch <huch@in.tum.de> / hgweb
  132. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  133. add ROOT checks for document presence and unused files; — Fabian Huch <huch@in.tum.de> / hgweb
  134. afp-submit visual improvements; — Fabian Huch <huch@in.tum.de> / hgweb
  135. update bibtex example; — Fabian Huch <huch@in.tum.de> / hgweb
  136. new doi — nipkow / hgweb
  137. sitegen for AOT — paulson <lp15@cam.ac.uk> / hgweb
  138. merged — paulson / hgweb
  139. New entry AOT — paulson <lp15@cam.ac.uk> / hgweb
  140. New entry: Propositional_Logic_Class — nipkow / hgweb
  141. sitegen for Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
  142. New entry Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
  143. Sorry — extra files for Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  144. Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  145. New entry Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
  146. New entry: Synthetic_Completeness — nipkow / hgweb
  147. New entry: Quantifier_Elimination_Hybrid — nipkow / hgweb
  148. New entry Birkhoff_Finite_Distributive_Lattices — nipkow / hgweb
  149. sitegen for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  150. metadata for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  151. new entry: Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  152. sitegen for Turan — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  153. added metadata for Turans graph theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  154. new entry: Turans Graph Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  155. new entry Multitape_To_Singletape_TM — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  156. removed static pages from rss feed; — Fabian Huch <huch@in.tum.de> / hgweb
  157. Minor rerating of the abstract of Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  158. sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  159. New entry Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
  160. sitegen for the aforementioned changes — paulson <lp15@cam.ac.uk> / hgweb
  161. adjustments to the abstract, requested by the author — paulson <lp15@cam.ac.uk> / hgweb
  162. CHERI-C_Memory_Model patch & metadata — paulson <lp15@cam.ac.uk> / hgweb
  163. New submission CHERI-C_Memory_Model — paulson <lp15@cam.ac.uk> / hgweb
  164. updated docs; — Fabian Huch <huch@in.tum.de> / hgweb
  165. improve page layout slightly; — Fabian Huch <huch@in.tum.de> / hgweb
  166. fixed broken abstract for PAPP_Impossibility — Manuel Eberl <manuel@pruvisto.org> / hgweb
  167. remove dead code — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  168. metadata and sitegen for PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  169. new entry PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  170. remove old .sitegen-ignore and mention AFP chapter in submission guidelines; — Fabian Huch <huch@in.tum.de> / hgweb
  171. afp_check_roots: proper error message printing; — Fabian Huch <huch@in.tum.de> / hgweb
  172. metadata and sitegen for Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  173. new entry: Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  174. tuned check names; — Fabian Huch <huch@in.tum.de> / hgweb
  175. make check roots tool less dependent on AFP structure; — Fabian Huch <huch@in.tum.de> / hgweb
  176. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  177. web for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  178. sitegen for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  179. New entry Combinatorial_Enumeration_Algorithms — nipkow / hgweb
  180. fix duplicate affiliations from author and notify; — Fabian Huch <huch@in.tum.de> / hgweb
  181. add metadata check tool to sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
  182. update check tools: add formatting checks, new cmd options; — Fabian Huch <huch@in.tum.de> / hgweb
  183. check for entries instead of session due to session nesting allowed in entries; — Fabian Huch <huch@in.tum.de> / hgweb
  184. added unused thy check; — Fabian Huch <huch@in.tum.de> / hgweb
  185. clarified check roots tool; — Fabian Huch <huch@in.tum.de> / hgweb
  186. afp-submit: tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
  187. afp-submit: encode new notify addresses properly; — Fabian Huch <huch@in.tum.de> / hgweb
  188. afp-submit: correct build status on empty file; — Fabian Huch <huch@in.tum.de> / hgweb
  189. afp-submit: remove padding on select; — Fabian Huch <huch@in.tum.de> / hgweb
  190. re-format metadata; — Fabian Huch <huch@in.tum.de> / hgweb
  191. afp-submit: update on correct status change; — Fabian Huch <huch@in.tum.de> / hgweb
  192. afp-submit: clarified date format, tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
  193. switch fonts to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
  194. switch to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
  195. clarified afp-submit error handling; — Fabian Huch <huch@in.tum.de> / hgweb
  196. clarified afp-submit creation and message; — Fabian Huch <huch@in.tum.de> / hgweb
  197. list submission system website; — Fabian Huch <huch@in.tum.de> / hgweb
  198. afp-submit: clarified api urls; — Fabian Huch <huch@in.tum.de> / hgweb
  199. Removal of more unused material — paulson <lp15@cam.ac.uk> / hgweb
  200. Small simplifications. Removed a needless assumption. — paulson <lp15@cam.ac.uk> / hgweb
  201. isabelle update -u cite; — wenzelm / hgweb
  202. more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc; — wenzelm / hgweb
  203. Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author) — paulson <lp15@cam.ac.uk> / hgweb
  204. merged — paulson / hgweb
  205. Added the missing .bib file — paulson <lp15@cam.ac.uk> / hgweb
  206. proper bib context for formal citations, although there is no document; — wenzelm / hgweb
  207. back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
  208. back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
  209. back to unchecked \cite: there is entry lacks .bib file; — wenzelm / hgweb
  210. proper citation; — wenzelm / hgweb
  211. merged — desharna / hgweb
  212. added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp] — desharna / hgweb
  213. merged — wenzelm / hgweb
  214. isabelle update -u cite; — wenzelm / hgweb
  215. merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
  216. consistent casing in \cite — Lars Hupel <lars.hupel@mytum.de> / hgweb
  217. ETTS: updated bibliography and citations — user9716869 <user9716869@gmail.com> / hgweb
  218. merged — wenzelm / hgweb
  219. more correct and complete citations; — wenzelm / hgweb
  220. unchecked \cite for unidentifiable citation; — wenzelm / hgweb
  221. proper @{cite} syntax; — wenzelm / hgweb
  222. isabelle update -u cite; — wenzelm / hgweb
  223. Updating Risk Free Lending Entry

      - Adding lemma for transfers in special case
      - Fixing grammar in abstract
      - Adding citation — Matthew Doty <matt@w-d.org> / hgweb
  224. added bibliography to ROOT; — Fabian Huch <huch@in.tum.de> / hgweb
  225. CTR and ETTS: several amendments (fact names, printing, presentation) — user9716869 <user9716869@gmail.com> / hgweb
  226. Removed a reference to the (redundant) wf_restr — paulson <lp15@cam.ac.uk> / hgweb
  227. added bibliographies to ROOTs; — Fabian Huch <huch@in.tum.de> / hgweb
  228. Changes for generalised lemmas — Katharina Kreuzer / hgweb
  229. Changes for generalised lemmas — Katharina Kreuzer / hgweb
  230. Generalised Lemmas — Katharina Kreuzer / hgweb
  231. merged — desharna / hgweb
  232. adapted to Isabelle/c9e091867206 — desharna / hgweb
  233. tuned; — wenzelm / hgweb
  234. tuned signature, following Isabelle/947510ce4e36; — wenzelm / hgweb
  235. adapted to Isabelle/25900fbea7ad;
    fewer clones of Isabelle sources; — wenzelm / hgweb
  236. adapted to Isabelle/b61ad889dffa — desharna / hgweb
  237. removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL — desharna / hgweb
  238. merged — desharna / hgweb
  239. adapted to Isabelle/d33fc5228aae — desharna / hgweb
  240. fixed proof following Isabelle/66cae055ac7b — desharna / hgweb
  241. merge — blanchet / hgweb
  242. adapted to Isabelle/c48fe2be847f — blanchet / hgweb
  243. enable -no-pie for CakeML — Lars Hupel <lars.hupel@mytum.de> / hgweb
  244. fixed proofs and removed duplicates following Isabelle/e65a50f6c2de — desharna / hgweb
  245. tuned proofs to use asymI, asymD, asympI, and asympD — desharna / hgweb
  246. Fix failing continuous integration — desharna / hgweb
  247. fixed proof following Isabelle/8fff4e4d81cb — desharna / hgweb
  248. removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL — desharna / hgweb
  249. added lemma imgu_range_vars_subset — desharna / hgweb
  250. Update headers and metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  251. Fix ROOT again — Asta Halkjær From <andro.from@gmail.com> / hgweb
  252. Fix ROOT — Asta Halkjær From <andro.from@gmail.com> / hgweb
  253. Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  254. Fixed proofs following Isabelle/a7d2a7a737b8 — desharna / hgweb
  255. added lemmas mem_range_varsI and imgu_subst_domain_subset — desharna / hgweb
  256. weakened the definition of redundant_inference — desharna / hgweb
  257. removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL — desharna / hgweb
  258. fixed Containers following introduction of irrefl_on — desharna / hgweb
  259. added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset — desharna / hgweb
  260. name change — nipkow / hgweb
  261. AFP and DBLP — nipkow / hgweb
  262. merged — desharna / hgweb
  263. added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset — desharna / hgweb
  264. added lemma subst_domain_rename_subst_domain_subset — desharna / hgweb
  265. added lemma image_the_Var_image_subst_renaming_eq — desharna / hgweb
  266. Added acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
  267. Added code export to ROOT — mohammadabdulaziz / hgweb
  268. Removed out of place code — mohammadabdulaziz / hgweb
  269. tuned lemma subst_domain_restrict_subst_domain — desharna / hgweb
  270. added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp] — desharna / hgweb
  271. added attribute [simp] to lemma rename_subst_domain_Var_rhs — desharna / hgweb
  272. added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp] — desharna / hgweb
  273. merged — desharna / hgweb
  274. removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL — desharna / hgweb
  275. removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL — desharna / hgweb
  276. added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp] — desharna / hgweb
  277. added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset — desharna / hgweb
  278. Streamlined a proof — paulson <lp15@cam.ac.uk> / hgweb
  279. added lemmas — desharna / hgweb
  280. moved lemma around — desharna / hgweb
  281. redefined mgu as a definition — desharna / hgweb
  282. tuned naming — desharna / hgweb
  283. fixed proof — desharna / hgweb
  284. added definition restrict_subst_domain and associated lemmas — desharna / hgweb
  285. tuned (sub)subsection — desharna / hgweb
  286. added lemma member_image_the_Var_image_subst — desharna / hgweb
  287. added lemmas unify_subst_domain_range_vars_disjoint — desharna / hgweb
  288. added lemma unify_range_vars — desharna / hgweb
  289. added lemma unify_subst_domain — desharna / hgweb
  290. added definition rename_subst_domain_range and related lemmas — desharna / hgweb
  291. merged — desharna / hgweb
  292. added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset — desharna / hgweb
  293. Fixed the ROOT file, so that the theory of cardinals is loaded — paulson <lp15@cam.ac.uk> / hgweb
  294. added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term — desharna / hgweb
  295. added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same — desharna / hgweb
  296. added lemma decompose_same_Fun[simp] — desharna / hgweb
  297. added lemma zip_option_same[simp] — desharna / hgweb
  298. added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain — desharna / hgweb
  299. removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
  300. used rho for renamming — desharna / hgweb
  301. tuned assumptions — desharna / hgweb
  302. added lemma subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
  303. added lemmas inv_renaming_sound and ex_inverse_of_renaming — desharna / hgweb
  304. added lemma subst_apply_term_ident — desharna / hgweb
  305. added lemmas subst_range_Var and range_vars_Var and moved stuff around — desharna / hgweb
  306. added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming — desharna / hgweb
  307. tuned naming — desharna / hgweb
  308. added lemma mgu_range_vars — desharna / hgweb
  309. added lemma subst_compose_apply_eq_apply_lhs_if — desharna / hgweb
  310. added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu — desharna / hgweb
  311. RealTimeDeque: replace `reverseN` with `take_rev — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  312. replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on — desharna / hgweb
  313. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  314. add missing thy files in Sturm_Tarski + repair — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  315. afp-submit: style page, improve elements; — Fabian Huch <huch@in.tum.de> / hgweb
  316. afp-submit: added repository updates; — Fabian Huch <huch@in.tum.de> / hgweb
  317. afp-submit: added download and faster file handling; — Fabian Huch <huch@in.tum.de> / hgweb
  318. add submission pages to web ui; — Fabian Huch <huch@in.tum.de> / hgweb
  319. afp-submit: add submission and build status with adapter to existing system; — Fabian Huch <huch@in.tum.de> / hgweb
  320. add user-facing exception handling to web app; — Fabian Huch <huch@in.tum.de> / hgweb
  321. clarified submission handling; — Fabian Huch <huch@in.tum.de> / hgweb
  322. afp-submit: added submission read-only and list views; — Fabian Huch <huch@in.tum.de> / hgweb
  323. add afp-submit web app; — Fabian Huch <huch@in.tum.de> / hgweb
  324. add web app facilities; — Fabian Huch <huch@in.tum.de> / hgweb
  325. RealTimeDeque: Separate implementation and auxiliary functions — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
  326. Backed out changeset 3a67df508397
    The finite simproc is no longer active by default — nipkow / hgweb
  327. adapted to new simproc finite — nipkow / hgweb
  328. clarified signature, following Isabelle/f362975e8ba1; — wenzelm / hgweb
  329. more direct Proof_Context.init_global; — wenzelm / hgweb
  330. proper naming conventions for Isabelle/ML; — wenzelm / hgweb
  331. Updated citation — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  332. merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  333. Isabelle2022: new release download links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  334. Added tag Isabelle2022 for changeset 548e384c0445 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  335. import 2022 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  336. entry names not restricted to alpha-numeric — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  337. add 2021-1 all releases; — Fabian Huch <huch@in.tum.de> / hgweb
  338. clarified docs — Fabian Huch <huch@in.tum.de> / hgweb
  339. replace old get-releases tool (now isabelle afp_release -I); — Fabian Huch <huch@in.tum.de> / hgweb
  340. add option for parallel session builds — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  341. set Isabelle2022 release date — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  342. set release version to 2022 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  343. merge from afp-2021-1 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  344. Removal of some old junk — paulson <lp15@cam.ac.uk> / hgweb
  345. Deleted unused material — paulson <lp15@cam.ac.uk> / hgweb
  346. nothing — paulson <lp15@cam.ac.uk> / hgweb
  347. Instantiation of the order solver for ⊑ and ⊏ (no real effect though) — paulson <lp15@cam.ac.uk> / hgweb
  348. proof simplifications — paulson <lp15@cam.ac.uk> / hgweb
  349. merged — paulson / hgweb
  350. Simplified the proofs a bit — paulson <lp15@cam.ac.uk> / hgweb
  351. merged — desharna / hgweb
  352. replaced fmember.rep_eq by fmember_iff_member_fset — desharna / hgweb
  353. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  354. only make parent dir; — Fabian Huch <huch@in.tum.de> / hgweb
  355. accept all dois; — Fabian Huch <huch@in.tum.de> / hgweb
  356. metadata toml: tuned error messages; — Fabian Huch <huch@in.tum.de> / hgweb
  357. clarified sub topics; — Fabian Huch <huch@in.tum.de> / hgweb
  358. adapted to Isabelle/457f1cba78fb — desharna / hgweb
  359. merged — desharna / hgweb
  360. added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;
    added simp annotation to generalizes_refl — desharna / hgweb
  361. extracted proof cases from lifting_lemma to distinct lemmas — desharna / hgweb
  362. tuned proof due to new simp rules — nipkow / hgweb
  363. corresponding lemma was removed from distribution — nipkow / hgweb
  364. regen site — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  365. updates to BenOr_Kozen_Reif by Katherine Kosaian — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  366. fix author entry; regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  367. add change history revision — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  368. Added scene spaces, improvements to prisms, and improvements to the alphabet command. — Simon Foster <simon.foster@york.ac.uk> / hgweb
  369. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  370. new entry Query_Optimization — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  371. remove temp file — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  372. Complex_Bounded_Operators: Various changes:

    - Removed auxiliary constant `the_riesz_rep_bilinear'`
    - Renamed constant `the_riesz_rep_bilinear` -> `the_riesz_rep_sesqui` and defined differently but equivalently
    - Renamed constant `bifunctional` -> `bidual_embedding`
      (and renamed lemmas containing `bifunctional` accordingly)
    - Renamed lemmas `the_riesz_rep_bilinear_apply` -> `the_riesz_rep_sesqui_apply`,
      `cblinfun_extension_exists_norm` -> `cblinfun_extension_norm_bounded_dense`
    - New theorems: `rank1_compose_left`, `rank1_compose_right`, `rank1_scaleC`,
      `rank1_uminus`, `rank1_uminus_iff`, `rank1_adj`, `rank1_adj_iff`,
      `bidual_embedding_surj`, `Cblinfun_comp_bounded_cbilinear`, `Cblinfun_comp_bounded_sesquilinear`, `bounded_clinear_0`,
      `bounded_antilinear_0`, `bounded_cbilinear_0`, `bounded_sesquilinear_0`, `bounded_cbilinear_apply_bounded_clinear`,
      `bounded_sesquilinear_apply_bounded_clinear`, `cblinfun_extension_exists_hilbert`,  `trunc_ell2_reduces_norm`,
      `trunc_ell2_add`, `trunc_ell2_scaleC`, `bounded_clinear_trunc_ell2`
    - Theorem `cblinfun_extension_exists_proj`: Reformulated one assumption — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  373. slightly less abusive proof pattern — haftmann / hgweb
  374. Many changes to entry `Complex_Bounded_Operators`:
    - Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`)
    - Cosmetic changes and cleanup of some proofs
    - Type class `one_dim` inherits from `complex_inner` now.
    - Moved various theorems around between theories
    - Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id`
    - Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere`
    - Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething
    - New definition: `rank1` (and lemmas about it)
    - New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`,
      `image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,
      `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`
    - Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),
      `cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`.
    - Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)

    Fixed entry `Registers` due to the changes above. — Dominique Unruh <unruh@ut.ee> / hgweb
  375. tuned proofs — haftmann / hgweb
  376. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  377. new entry Undirected_Graph_Theory — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  378. typo — nipkow / hgweb
  379. typo — nipkow / hgweb
  380. New entry: Maximum_Segment_Sum — nipkow / hgweb
  381. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  382. added topic for data management systems; — Fabian Huch <huch@in.tum.de> / hgweb
  383. added missing file — nipkow / hgweb
  384. New entry Safe_Range_RC — nipkow / hgweb
  385. adjust Stalnaker_Logic to changes in Epistemic_Logic; — Fabian Huch <huch@in.tum.de> / hgweb
  386. adjusted to distribution — haftmann / hgweb
  387. remove duplicate code; — Fabian Huch <huch@in.tum.de> / hgweb
  388. restructure afp ci builds (see Isabelle/3c4e373922ca) — Fabian Huch <huch@in.tum.de> / hgweb
  389. Cosmetic changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  390. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  391. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  392. afp site: minor stylistic improvements; — Fabian Huch <huch@in.tum.de> / hgweb
  393. web entry for Stalnaker_Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  394. new entry: Stalnaker Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  395. clarified options, following f2094906e491; — wenzelm / hgweb
  396. Comments on theories brought from ZF-Constructible. Shortening fm names — sterraf / hgweb
  397. adjusted to distribution — haftmann / hgweb
  398. Remove fontenc from root.tex to make Ł show in PDF. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  399. Update ROOT... — Asta Halkjær From <andro.from@gmail.com> / hgweb
  400. Appendix with another axiom system as a variant of the proof. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  401. adapt to Isabelle@769a7cd5a16a — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  402. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  403. adjust Lar's contact info as requested — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  404. sitegen for Padic_Field — Manuel Eberl <manuel@pruvisto.org> / hgweb
  405. new entry: Padic_Field — Manuel Eberl <manuel@pruvisto.org> / hgweb
  406. sitegen for Risk_Free_Lending — Manuel Eberl <manuel@pruvisto.org> / hgweb
  407. new entry: Risk_Free_Lending — Manuel Eberl <manuel@pruvisto.org> / hgweb
  408. new entry Implicational_Logic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  409. New entry Separation_Logic_Unbounded — nipkow / hgweb
  410. added web files — nipkow / hgweb
  411. added web files — nipkow / hgweb
  412. New entry SCC_Bloemen_Sequential — nipkow / hgweb
  413. A few more disambiguations, related to locales in CartesianCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  414. Merged — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  415. Further disambiguation of facts to address clashes involving ConcreteCategory as a sublocale. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  416. streamlined division on polynomials — haftmann / hgweb
  417. Complex_Bounded_Operators: Fixed errors in document generation — Dominique Unruh <unruh@ut.ee> / hgweb
  418. Complex_Bounded_Operators: Added numerous new lemmas. — Dominique Unruh <unruh@ut.ee> / hgweb
  419. Merged — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  420. Disambiguate sufficiently many facts in locales so as to permit a top-level interpretation of ZFC_set_cat. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  421. Fix a typo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  422. Neater links — Asta Halkjær From <andro.from@gmail.com> / hgweb
  423. Relational_Disjoint_Set_Forests: variant abstraction — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  424. merged — wenzelm / hgweb
  425. support for ISABELLE_MLTON_OPTIONS, following Isabelle/d27ed188e0c4; — wenzelm / hgweb
  426. Renaming synthesized formulas — sterraf / hgweb
  427. prefer (smt (verit)), which is potentially more stable under heavy load; — wenzelm / hgweb
  428. Add additional results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  429. Formatting. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  430. Add papers to abstracts. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  431. merged — paulson / hgweb
  432. Purely cosmetic — paulson <lp15@cam.ac.uk> / hgweb
  433. merged — paulson / hgweb
  434. Deleted one redundant step — paulson <lp15@cam.ac.uk> / hgweb
  435. merged — paulson / hgweb
  436. Merge — paulson <lp15@cam.ac.uk> / hgweb
  437. Tidied (a lot) — paulson <lp15@cam.ac.uk> / hgweb
  438. added missing congruence rule — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  439. streamlined — haftmann / hgweb
  440. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; — wenzelm / hgweb
  441. tuned whitespace; — wenzelm / hgweb
  442. merged — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  443. some slight polishing in the UTM entry — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  444. added congruence rule for forallM of Error-Monad — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  445. updated to devel — nipkow / hgweb
  446. merged — wenzelm / hgweb
  447. tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; — wenzelm / hgweb
  448. removed obsolete workaround (see Isabelle/91ee232b4211); — wenzelm / hgweb
  449. Eliminated the temporary material that was already migrated to the Isabelle libraries — paulson <lp15@cam.ac.uk> / hgweb
  450. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  451. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  452. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  453. merged — paulson / hgweb
  454. New entry CRYSTALS-Kyber — paulson <lp15@cam.ac.uk> / hgweb
  455. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  456. added missing history in metadata; — Fabian Huch <huch@in.tum.de> / hgweb
  457. retrieve missing change history in metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
  458. backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726 — Fabian Huch <huch@in.tum.de> / hgweb
  459. new email address for Maksym — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  460. metadata and sitegen for Khovansikii_Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  461. new entry: Khovanski-Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  462. fixed metadata for Hales_Jewett — Manuel Eberl <manuel@pruvisto.org> / hgweb
  463. sitegen for Number_Theoretic_Transform — Manuel Eberl <manuel@pruvisto.org> / hgweb
  464. new entry Number_Theoretic_Transform — Manuel Eberl <manuel@pruvisto.org> / hgweb
  465. new entry Hales Jewett — nipkow / hgweb
  466. adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089); — Fabian Huch <huch@in.tum.de> / hgweb
  467. updated entry for Universal Turing Machines — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  468. merged — desharna / hgweb
  469. adapted to antimono — desharna / hgweb
  470. merged — desharna / hgweb
  471. adapted to new mono and strict_mono — desharna / hgweb
  472. updated to Isabelle/5ea588440b06 — desharna / hgweb
  473. Updated citations — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  474. Updated citations — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  475. tuned signature; — wenzelm / hgweb
  476. merged — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  477. Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  478. tuned timeouts, based on test runs with threads=1; — wenzelm / hgweb
  479. replaced slow smt call by blast — blanchet / hgweb
  480. avoid hardwired document; — wenzelm / hgweb
  481. merged — paulson / hgweb
  482. cosmetic — paulson <lp15@cam.ac.uk> / hgweb
  483. replace smt_oracle by proper veriT reconstruction — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  484. merged — paulson / hgweb
  485. tweaks — paulson <lp15@cam.ac.uk> / hgweb
  486. make all sessions of chapter "AFP" belong to group "AFP"; — wenzelm / hgweb
  487. chapter_definition for presentation; — wenzelm / hgweb
  488. Undo an unrelated change that somehow crept into the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  489. Remove lots of unnecessary explicit quantifiers in lemma statements, now that I've discovered "arbitrary:". — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  490. Revised locale structure and notation. Proposed modularization for ZF-Constructible's M_eclose — sterraf / hgweb
  491. tuning — blanchet / hgweb
  492. updated entries: Combinatorics_Words, Combinatorics_Words_Lyndon, and Combinatorics_Words_Graph_Lemma — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / hgweb
  493. avoid fact name clash — haftmann / hgweb
  494. adjusted to distribution — haftmann / hgweb
  495. repaired proof — haftmann / hgweb
  496. Complex_Bounded_Operators: Fixed document generation — Dominique Unruh <unruh@ut.ee> / hgweb
  497. Merged changes. — Dominique Unruh <unruh@ut.ee> / hgweb
  498. Registers: Fixed parse error. — Dominique Unruh <unruh@ut.ee> / hgweb
  499. Misc updates to Complex_Bounded_Operators:

    Many new lemmas.
    New definitions: cblinfun_power, cblinfun_left, cblinfun_right, ccsubspace_Times, partial_isometry, the_riesz_rep, the_riesz_rep_bilinear', the_riesz_rep_bilinear, bij_between_bases, unitary_between, is_onb, some_chilbert_basis, rel_ccsubspace.
    instance prod :: complex_normed_vector.
    Changed infix priority of oCL to 67.
    Changed local structure: Complex locales now are sublocales of real locals with prefix real.
    Renamed norm_blinfun_id_le -> norm_cblinfun_id_le. — Dominique Unruh <unruh@ut.ee> / hgweb
  500. Reintroduce type signatures. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  501. Switch to simultaneous substitutions. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  502. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  503. new entry: Nano_JSON — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  504. sitegen for Commuting_Hermitian — Manuel Eberl <manuel@pruvisto.org> / hgweb
  505. new entry: Commuting_Hermitian — Manuel Eberl <manuel@pruvisto.org> / hgweb
  506. Sitegen for Involutions2Squares (WITH WRONG EMAIL ADDRESS) — paulson <lp15@cam.ac.uk> / hgweb
  507. new entry Involutions2Squares — paulson <lp15@cam.ac.uk> / hgweb
  508. fix typo — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  509. new entry Solidity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  510. tuned title — nipkow / hgweb
  511. more typos — nipkow / hgweb
  512. regenerate because of typos — nipkow / hgweb
  513. New entry — nipkow / hgweb
  514. topics no longer exist — nipkow / hgweb
  515. new topics — nipkow / hgweb
  516. New entry FSM_Tests — nipkow / hgweb
  517. merged — wenzelm / hgweb
  518. Isabelle/b6589c8ccadd officially supports README.thy; — wenzelm / hgweb
  519. streamlined — haftmann / hgweb
  520. tuned proofs — haftmann / hgweb
  521. discontinued obsolete README.html: superseded by abstract provided by AFP; — wenzelm / hgweb
  522. streamlined primitive definitions for integer division — haftmann / hgweb
  523. tuned code equations for Xml-parsing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  524. refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so that real and complex numbers work) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  525. Revision of locale structure — sterraf / hgweb
  526. Purely markup — paulson <lp15@cam.ac.uk> / hgweb
  527. Fix ImpSplit thy for document generation — Niels Mündler <n.muendler@web.de> / hgweb
  528. Add B+Tree formalisation to the BTree entry — Niels Mündler <n.muendler@web.de> / hgweb
  529. Correcting thm antiquotations. Turning code comments into text — sterraf / hgweb
  530. Update metadata and root.tex to mention the addition of ZFC_SetCat in early 2022. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  531. Sync with my development repo:  Category3: add various rules for limits.  RTS: strengthen definition of transformation. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  532. adapted to NLists.thy — nipkow / hgweb
  533. merged — nipkow / hgweb
  534. use Library/NList.thy now — nipkow / hgweb
  535. Further streamlining of quick-and-dirty evaluation. — haftmann / hgweb
  536. An attempt for an integrated solution for quick-and-dirty evaluation. — haftmann / hgweb
  537. Further reduction of locale assumptions — sterraf / hgweb
  538. merged — wenzelm / hgweb
  539. more complete theorem_commands; — wenzelm / hgweb
  540. clarified signature, following Isabelle/b6d74c90b588; — wenzelm / hgweb
  541. Update metadata for Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
  542. merged — Richard Schmoetten <richard.schmoetten@ed.ac.uk> / hgweb
  543. Update Schutz_Spacetime

    chain (and other) definitions, notations, extra gorder proof, general cleanup

    corresponds to revisions to JAR paper — Richard Schmoetten <richard.schmoetten@ed.ac.uk> / hgweb
  544. more accurate name — blanchet / hgweb
  545. more politically correct — blanchet / hgweb
  546. two new lemmas — paulson <lp15@cam.ac.uk> / hgweb
  547. added two lemmas to relational chains — blanchet / hgweb
  548. changed confusing assumption name — blanchet / hgweb
  549. avoid the surprise that n-m is 0 even if n<m. — nipkow / hgweb
  550. tuned — nipkow / hgweb
  551. simplified invar — nipkow / hgweb
  552. merged — nipkow / hgweb
  553. simplified — nipkow / hgweb
  554. update metadata; — wenzelm / hgweb
  555. merged — nipkow / hgweb
  556. tuned — nipkow / hgweb
  557. removed a spurious locale parameter -- the same issue probably arises in the pen-and-paper Waldmann et al. — blanchet / hgweb
  558. removed needless assumption — blanchet / hgweb
  559. Named intermediate results combinable wands — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  560. Named intermediate results Package logic — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
  561. added lemma about lazy list chains — blanchet / hgweb
  562. typo — blanchet / hgweb
  563. Refining three sessions.
    * Delta_System_Lemma: Moving results out of the scope of AC.
    * Transitive_Models: General locale re-engineering.
    * Independence_CH: specifying finite set of axioms required for
      forcing CH and ¬CH. — sterraf / hgweb
  564. Tuned. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  565. merged — nipkow / hgweb
  566. addd DOIs and other metadata links — nipkow / hgweb
  567. some slight polishing of the definitions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  568. added links — nipkow / hgweb
  569. added metadata links — nipkow / hgweb
  570. added link — nipkow / hgweb
  571. added Wiki link — nipkow / hgweb
  572. added DOIs — nipkow / hgweb
  573. added DIs — nipkow / hgweb
  574. added DOIs — nipkow / hgweb
  575. Added DOIs — nipkow / hgweb
  576. added DOIs — nipkow / hgweb
  577. added DOIs — nipkow / hgweb
  578. merged — nipkow / hgweb
  579. added DOIs — nipkow / hgweb
  580. XZ compression for Safe_Distance examples (safes 160 MB!) — Manuel Eberl <eberlm@in.tum.de> / hgweb
  581. tuned DOIs — nipkow / hgweb
  582. added DOIs — nipkow / hgweb
  583. added DOIs — nipkow / hgweb
  584. added DOIs — nipkow / hgweb
  585. added pubs — nipkow / hgweb
  586. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  587. improve DOI resolving: offline cache and better timeouts; — Fabian Huch <huch@in.tum.de> / hgweb
  588. added pubs — nipkow / hgweb
  589. added DOIs — nipkow / hgweb
  590. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  591. resolve DOIs in sitegen to formatted citations; — Fabian Huch <huch@in.tum.de> / hgweb
  592. removed links from related references; — Fabian Huch <huch@in.tum.de> / hgweb
  593. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  594. Remove duplication between Universal_Hash_Families (UHF) and Finite_Fields (FF).

    - Also remove white space in UHF. — Emin Karayel <me@eminkarayel.de> / hgweb
  595. Update metadata for WOOT_Strong_Eventual_Consistency.

    - Added corresponding publication in related works.
    - Added orcid id's of authors. — Emin Karayel <me@eminkarayel.de> / hgweb
  596. added DOI — nipkow / hgweb
  597. added DOI — nipkow / hgweb
  598. merged — nipkow / hgweb
  599. added orcid — nipkow / hgweb
  600. added orcid — nipkow / hgweb
  601. added lemma — nipkow / hgweb
  602. ORCID for Manuel Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
  603. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  604. updated help page; — Fabian Huch <huch@in.tum.de> / hgweb
  605. clarified doc; — Fabian Huch <huch@in.tum.de> / hgweb
  606. name change for Kądziołka — Manuel Eberl <manuel@pruvisto.org> / hgweb
  607. updated docs on metadata; — Fabian Huch <huch@in.tum.de> / hgweb
  608. adjusted topics and added subject classifications; — Fabian Huch <huch@in.tum.de> / hgweb
  609. name change for Kądziołka — Manuel Eberl <manuel@pruvisto.org> / hgweb
  610. moved lemma to distribution — nipkow / hgweb
  611. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  612. added more metadata fields: related references for entries, orcids for authors, and acm/ams subject classification for topics; — Fabian Huch <huch@in.tum.de> / hgweb
  613. tuned topics — nipkow / hgweb
  614. adjusted topics — nipkow / hgweb
  615. proper license link; — Fabian Huch <huch@in.tum.de> / hgweb
  616. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  617. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  618. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  619. sitegen: integrate change history and note properly; — Fabian Huch <huch@in.tum.de> / hgweb
  620. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  621. clarified homepage urls; — Fabian Huch <huch@in.tum.de> / hgweb
  622. remove metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
  623. toml parser improvements: comments are now treated as whitespace. — Fabian Huch <huch@in.tum.de> / hgweb
  624. clarified metadata loading and added more metadata checks; — Fabian Huch <huch@in.tum.de> / hgweb
  625. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  626. improve releases view and map correctly to Isabelle version; — Fabian Huch <huch@in.tum.de> / hgweb
  627. add missing releases again; — Fabian Huch <huch@in.tum.de> / hgweb
  628. merged — paulson / hgweb
  629. sitegen for Weighted_Arithmetic_Geometric_Mean — paulson <lp15@cam.ac.uk> / hgweb
  630. new entry Weighted_Arithmetic_Geometric_Mean — paulson <lp15@cam.ac.uk> / hgweb
  631. missing file — nipkow / hgweb
  632. New entry IMP_Compiler_Reuse — nipkow / hgweb
  633. Just variable renamings — paulson <lp15@cam.ac.uk> / hgweb
  634. merged — paulson / hgweb
  635. Simplified and shortened some proofs — paulson <lp15@cam.ac.uk> / hgweb
  636. moved lemmas to distribution — nipkow / hgweb
  637. merged — paulson / hgweb
  638. tweaked — paulson <lp15@cam.ac.uk> / hgweb
  639. merged — paulson / hgweb
  640. a bit of tidying — paulson <lp15@cam.ac.uk> / hgweb
  641. cleanup with global-interpretations and code equations in Simplex_Incremental — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  642. changed incremental simplex interface: check now always returns a new state, even in unsat-case — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  643. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  644. Improvements. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  645. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  646. sitegen: tuned statistics; — Fabian Huch <huch@in.tum.de> / hgweb
  647. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  648. sitegen for Boolos_Curious_Inference — paulson <lp15@cam.ac.uk> / hgweb
  649. new entry: Boolos_Curious_Inference — paulson <lp15@cam.ac.uk> / hgweb
  650. website: proper bibtex entries; — Fabian Huch <huch@in.tum.de> / hgweb
  651. tuned — haftmann / hgweb
  652. removed more material now residing in distribution — haftmann / hgweb
  653. separated non-computable instance of bit comprehension from computable one — haftmann / hgweb
  654. Small changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  655. Undo accidental changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  656. Tuned. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  657. tuned -- follow clone in $ISABELLE_HOME/src/HOL/Imperative_HOL/Heap_Monad.thy; — wenzelm / hgweb
  658. minor performance tuning: avoid redundant BigInt construction; — wenzelm / hgweb
  659. prefer self-made Array.T, to avoid problems with ArraySeq in Scala 3; — wenzelm / hgweb
  660. more robust Array.T for Scala 2.13 and 3.x, following Isabelle/ca450d902198; — wenzelm / hgweb
  661. Move code lemmas for symbolic computation of bit operations on int to distribution. — haftmann / hgweb
  662. renamings — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  663. Relational_Disjoint_Set_Forests: improved abstractions — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  664. Simplified a proof using Cauchy–Schwarz — paulson <lp15@cam.ac.uk> / hgweb
  665. removed precondition in det_four_block_mat — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  666. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  667. removed assumption in det_bound_hadamard_tight, moved some basic lemmas on matrices, added a conditional version of det(four_block_mat ...) = ... — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  668. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  669. updated doc; — Fabian Huch <huch@in.tum.de> / hgweb
  670. regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
  671. obfuscate email addresses in metadata and generated site; — Fabian Huch <huch@in.tum.de> / hgweb
  672. renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  673. added lemma for special case of small integer solutions (no mixed integer), where then everything is of type int — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  674. document change in metadata — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  675. generalized fixed bounds on determinants to predicate; added an improved determinate bound
    -> result: get smaller bound on mixed integer solutions  (replace n! by sqrt(n^n)) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  676. Code generated in the same directory — mohammadabdulaziz / hgweb
  677. Removed ML code from AFP entry — mohammadabdulaziz / hgweb
  678. adapted to scala-3.1.2; — wenzelm / hgweb
  679. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  680. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  681. tooling: added utility to check for metadata consistency; — Fabian Huch <huch@in.tum.de> / hgweb
  682. regenerate website; — Fabian Huch <huch@in.tum.de> / hgweb
  683. site: generate multi-line json for smaller merges; — Fabian Huch <huch@in.tum.de> / hgweb
  684. toml module: proper parsing of quotes in multiline strings; — Fabian Huch <huch@in.tum.de> / hgweb
  685. added further sitegen generated websites — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  686. added metadata for Real_Time_Deque's, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  687. new entry: Real-Time Double-Ended Queue — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  688. merged — desharna / hgweb
  689. replaced IMGU by min_IMGU — desharna / hgweb
  690. replaced MGU by IMGU — desharna / hgweb
  691. exposed that inverse of renaming only maps variables to variables — desharna / hgweb
  692. added the r{n..} regular expression to the extensions directory in the Posix-Lexing entry, added two small lemmas to the Regular-Set theory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  693. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  694. regenerate website — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  695. do not ignore admin/site — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  696. remove afp python component build tool; — Fabian Huch <huch@in.tum.de> / hgweb
  697. afp tooling: improve keyword extraction; — Fabian Huch <huch@in.tum.de> / hgweb
  698. website: small improvements; — Fabian Huch <huch@in.tum.de> / hgweb
  699. tuned efficiency of XML parser — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  700. tuned — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  701. updated the abstract in root.tex — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  702. added the r{..n} regular expression to the extensions directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  703. merged — traytel / hgweb
  704. tuned BNF bound — traytel / hgweb
  705. strict bounds for BNFs (by Jan van Brügge) — traytel / hgweb
  706. merge from afp-2021-1 (replaying devel commit) — Fabian Huch <huch@in.tum.de> / hgweb
  707. replaced python RAKE component with Isabelle/Scala Rake component; — Fabian Huch <huch@in.tum.de> / hgweb
  708. remove scala tools from publish; — Fabian Huch <huch@in.tum.de> / hgweb
  709. replaced python RAKE component with Isabelle/Scala Rake component; — Fabian Huch <huch@in.tum.de> / hgweb
  710. merged — wenzelm / hgweb
  711. avoid hardwired pdf; — wenzelm / hgweb
  712. adapted to Isabelle/986506233812; — wenzelm / hgweb
  713. merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  714. added an implementation of pseudo remainder sequences for calculating Tarski queries — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  715. merged — desharna / hgweb
  716. updated to Isabelle/3c544d64c218 — desharna / hgweb
  717. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  718. tuned error messages; — Fabian Huch <huch@in.tum.de> / hgweb
  719. mention error location when metadata loading fails; — Fabian Huch <huch@in.tum.de> / hgweb
  720. merged — Fabian Huch <huch@in.tum.de> / hgweb
  721. even more IsaNet; — Fabian Huch <huch@in.tum.de> / hgweb
  722. afp metadata/releases: change format to re-add releases swallowed by key-set, remove extra releases; — Fabian Huch <huch@in.tum.de> / hgweb
  723. more IsaNet — nipkow / hgweb
  724. New entry IsaNet — nipkow / hgweb
  725. adapted to Isabelle/39df30349778; — wenzelm / hgweb
  726. added extension that deals with the n-times regular expression in Posix-Lexing — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  727. Avoid calculations where not necessary. — haftmann / hgweb
  728. used long version of definition to avoid conflict when introducing HOL.monotone_on — desharna / hgweb
  729. merge from afp-2021-1 (metadata consolidation) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  730. sitegen — nipkow / hgweb
  731. unified home pages — nipkow / hgweb
  732. re-introduce accidentally reverted changes — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  733. ignore dev site output — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  734. consolidate metadata (email and homepages) — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  735. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  736. load mail configuration lazily (initialized later from properties); — Fabian Huch <huch@in.tum.de> / hgweb
  737. tuned home pages — nipkow / hgweb
  738. merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
  739. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  740. proper topics loading; — Fabian Huch <huch@in.tum.de> / hgweb
  741. merge from afp-2021-1 (new website) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  742. new website — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  743. admin: remove old sitegen lib files — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  744. update metadata to new sitegen — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  745. merge website-redesign graft — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
  746. updated afp sitegen doc; — Fabian Huch <huch@in.tum.de> / hgweb
  747. replaced python afp stats with Isabelle/Scala tool; — Fabian Huch <huch@in.tum.de> / hgweb
  748. updated afp metadata doc (now as markdown); — Fabian Huch <huch@in.tum.de> / hgweb
  749. afp components: removed unnecessary platforms; — Fabian Huch <huch@in.tum.de> / hgweb
  750. afp sitegen: switch to new version; — Fabian Huch <huch@in.tum.de> / hgweb
  751. add sitegen ignore option; — Fabian Huch <huch@in.tum.de> / hgweb
  752. improvements for toml module: proper boolean values; — Fabian Huch <huch@in.tum.de> / hgweb
  753. add components as proper afp deps; — Fabian Huch <huch@in.tum.de> / hgweb
  754. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  755. switched to standalone cross-platform afp python component; — Fabian Huch <huch@in.tum.de> / hgweb
  756. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  757. afp python build: use tgz for better cross-plattform compatability; — Fabian Huch <huch@in.tum.de> / hgweb
  758. replaced ci_profiles by statically compiled afp_build tool (Scala 3 preparations); — Fabian Huch <huch@in.tum.de> / hgweb
  759. afp structure: added accessors; — Fabian Huch <huch@in.tum.de> / hgweb
  760. hugo site: minor changes; — Fabian Huch <huch@in.tum.de> / hgweb
  761. hugo-site: improve various aspects; — Fabian Huch <huch@in.tum.de> / hgweb
  762. add new authors to migration; — Fabian Huch <huch@in.tum.de> / hgweb
  763. clarified formatting, for the sake of scala3; — Fabian Huch <huch@in.tum.de> / hgweb
  764. hugo site: better scrolling; — Fabian Huch <huch@in.tum.de> / hgweb
  765. hugo site: updated devel info; — Fabian Huch <huch@in.tum.de> / hgweb
  766. hugo site: updated content; — Fabian Huch <huch@in.tum.de> / hgweb
  767. hugo site: proper ordering; — Fabian Huch <huch@in.tum.de> / hgweb
  768. hugo site: restricted generated affiliations;
    hugo site: added fresh option; — Fabian Huch <huch@in.tum.de> / hgweb
  769. hugo site: proper theory view link scrolling; — Fabian Huch <huch@in.tum.de> / hgweb
  770. hugo site: tuned affiliation keys; — Fabian Huch <huch@in.tum.de> / hgweb
  771. hugo site: proper topic-only topics page; — Fabian Huch <huch@in.tum.de> / hgweb
  772. hugo site: relativize paths; — Fabian Huch <huch@in.tum.de> / hgweb
  773. hugo site: list sessions separately; — Fabian Huch <huch@in.tum.de> / hgweb
  774. hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  775. hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  776. hugo site: merge gen and build tool; — Fabian Huch <huch@in.tum.de> / hgweb
  777. hugo site: added doc headers; — Fabian Huch <huch@in.tum.de> / hgweb
  778. hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  779. afp metadata: index keys for emails and urls;
    apf metadata: separate license file; — Fabian Huch <huch@in.tum.de> / hgweb
  780. hugo site: improve theory view; — Fabian Huch <huch@in.tum.de> / hgweb
  781. hugo site: cleaned up; — Fabian Huch <huch@in.tum.de> / hgweb
  782. hugo site: added devel version; — Fabian Huch <huch@in.tum.de> / hgweb
  783. hugo site: updated search and content; — Fabian Huch <huch@in.tum.de> / hgweb
  784. hugo site: added theory view styling for different device sizes;
    hugo site: update contributions; — Fabian Huch <huch@in.tum.de> / hgweb
  785. Updated metadata in migration and theory view; — Fabian Huch <huch@in.tum.de> / hgweb
  786. hugo site: updated site templates; — Fabian Huch <huch@in.tum.de> / hgweb
  787. metadata migration: updated authors; — Fabian Huch <huch@in.tum.de> / hgweb
  788. hugo: added mobile view; — Fabian Huch <huch@in.tum.de> / hgweb
  789. hugo: copy to proper path; — Fabian Huch <huch@in.tum.de> / hgweb
  790. added theory navbar; — Fabian Huch <huch@in.tum.de> / hgweb
  791. tuned formatting; — Fabian Huch <huch@in.tum.de> / hgweb
  792. added loader; — Fabian Huch <huch@in.tum.de> / hgweb
  793. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  794. tuned: more canonical Isabelle code style; — Fabian Huch <huch@in.tum.de> / hgweb
  795. proper loading of foundational hrefs; — Fabian Huch <huch@in.tum.de> / hgweb
  796. fix dependencies; — Fabian Huch <huch@in.tum.de> / hgweb
  797. added devel flag; — Fabian Huch <huch@in.tum.de> / hgweb
  798. updated about page; — Fabian Huch <huch@in.tum.de> / hgweb
  799. moved extraction of related entries to hugo; — Fabian Huch <huch@in.tum.de> / hgweb
  800. improved keyword extraction; — Fabian Huch <huch@in.tum.de> / hgweb
  801. added keywords to site generated entry data; — Fabian Huch <huch@in.tum.de> / hgweb
  802. use tmp file for python script instead of command; — Fabian Huch <huch@in.tum.de> / hgweb
  803. added js-side theory loading to afp site; — Fabian Huch <huch@in.tum.de> / hgweb
  804. integrated metadata changes into site;
    tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  805. added missing keyword data; — Fabian Huch <huch@in.tum.de> / hgweb
  806. removed html dir from sitegen (now set inside hugo); — Fabian Huch <huch@in.tum.de> / hgweb
  807. tuned sitegen: moved dependencies generation to scala — Fabian Huch <huch@in.tum.de> / hgweb
  808. changed generated author format; — Fabian Huch <huch@in.tum.de> / hgweb
  809. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  810. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  811. tuned hugo: static files more explicit; — Fabian Huch <huch@in.tum.de> / hgweb
  812. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  813. proper authors/affiliations gen for hugo taxonomy; — Fabian Huch <huch@in.tum.de> / hgweb
  814. clarified hugo data; — Fabian Huch <huch@in.tum.de> / hgweb
  815. added missing name mapping to migration; — Fabian Huch <huch@in.tum.de> / hgweb
  816. proper output path; — Fabian Huch <huch@in.tum.de> / hgweb
  817. added missing topics; — Fabian Huch <huch@in.tum.de> / hgweb
  818. clarified hugo build signature;
    split site generation into own afp site gen tool; — Fabian Huch <huch@in.tum.de> / hgweb
  819. added more steps to afp site generation tool; — Fabian Huch <huch@in.tum.de> / hgweb
  820. tuned;
    clarified hugo; — Fabian Huch <huch@in.tum.de> / hgweb
  821. added hugo project by Carlin MacKenzie; — Fabian Huch <huch@in.tum.de> / hgweb
  822. added sitegen scripts by Carlin MacKenzie (slightly tweaked); — Fabian Huch <huch@in.tum.de> / hgweb
  823. added afp hugo module; — Fabian Huch <huch@in.tum.de> / hgweb
  824. clarified afp_dependencies: proper typed output;
    added afp_dependencies json module; — Fabian Huch <huch@in.tum.de> / hgweb
  825. Added afp structure module; — Fabian Huch <huch@in.tum.de> / hgweb
  826. Added python wrapper; — Fabian Huch <huch@in.tum.de> / hgweb
  827. clarified metadata; — Fabian Huch <huch@in.tum.de> / hgweb
  828. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  829. added afp hugo component; — Fabian Huch <huch@in.tum.de> / hgweb
  830. added afp python component with required packages; — Fabian Huch <huch@in.tum.de> / hgweb
  831. feat(afp/tools): added initial site build tool — Fabian Huch <huch@in.tum.de> / hgweb
  832. tuned(afp/tools): metadata sorted — Fabian Huch <huch@in.tum.de> / hgweb
  833. tuned(afp/tools): tuned parser/unparser — Fabian Huch <huch@in.tum.de> / hgweb
  834. feat(afp/tools): more metadata and toml conversion; — Fabian Huch <huch@in.tum.de> / hgweb
  835. feat(afp/tools): added TOML lexer and parser; — Fabian Huch <huch@in.tum.de> / hgweb
  836. tuned(afp/tools): module jar locations; — Fabian Huch <huch@in.tum.de> / hgweb
  837. fix(afp/tools): added missing metadata, improved toml structure — Fabian Huch <huch@in.tum.de> / hgweb
  838. fix(afp/tools): removed TOML formatting heuristics for simplicity; — Fabian Huch <huch@in.tum.de> / hgweb
  839. feat(afp/tools): added TOML module; — Fabian Huch <huch@in.tum.de> / hgweb
  840. feat(afp/tools): added metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
  841. feat(afp/tools): migrated scala tool_bodys to proper tools; — Fabian Huch <huch@in.tum.de> / hgweb
  842. Avoid explicit operation when not necessary. — haftmann / hgweb
  843. adjust for isabelle@5bba3516ddb5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  844. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  845. Added a missing acknowledgement — paulson <lp15@cam.ac.uk> / hgweb
  846. metadata for Finite_Fields (and missing <> for two previous entries) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  847. new entry: Finite_Fields — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  848. sitegen for DPRM_Theorem — paulson <lp15@cam.ac.uk> / hgweb
  849. DPRM_Theorem: finally cleaned up and impressive! — paulson <lp15@cam.ac.uk> / hgweb
  850. New entry [Rewrite_Properties_Reduction] — nipkow / hgweb
  851. Fixed broken LaTeX in the abstract — paulson <lp15@cam.ac.uk> / hgweb
  852. sitegen for Combinable_Wands — paulson <lp15@cam.ac.uk> / hgweb
  853. New entry Combinable_Wands — paulson <lp15@cam.ac.uk> / hgweb
  854. corrected metadata (separate authors by "," not by "and") — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  855. sitegen and metadata for Pluennecke_Ruzsa_Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  856. new entry: Pluennecke Ruzsa Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  857. Tuning the abstract to remove some of the display mathematics — paulson <lp15@cam.ac.uk> / hgweb
  858. sitegen for Package_logic — paulson <lp15@cam.ac.uk> / hgweb
  859. new entry Package_logic — paulson <lp15@cam.ac.uk> / hgweb
  860. Removal of all email addresses, at authors' request — paulson <lp15@cam.ac.uk> / hgweb
  861. renamed some variables — paulson <lp15@cam.ac.uk> / hgweb
  862. proper \open\close markup — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  863. Updated the Posix-Lexer entry including a small change in Regular-Set — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
  864. Trimmed down dependencies. — haftmann / hgweb
  865. Merge equivalent instance declarations for functions in Lp.Functional_Spaces and HOL-Library.Function_Algebras.

    Because of the distinct but equivalent instance declarations in the mentioned theories, it was not possible to import both libraries at the same time.
    This commit fixes the problem. — Emin Karayel <me@eminkarayel.de> / hgweb
  866. Remove duplicate lemma and fix typos in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
  867. same variant as for imperative algorithm to prove n^2 complexity — nipkow / hgweb
  868. tuned — nipkow / hgweb
  869. Shortened and simplified a proof — paulson <lp15@cam.ac.uk> / hgweb
  870. more realistic timeout; — wenzelm / hgweb
  871. tuned whitespace; — wenzelm / hgweb
  872. more realistic timeout;
    more parallelism; — wenzelm / hgweb
  873. avoid hard-wired document; — wenzelm / hgweb
  874. removed usages of HOL.no_atp as its content and order is not guaranteed — desharna / hgweb
  875. cleaning — nipkow / hgweb
  876. no separate code-equations required for a lift_definition by using (code_dt) instead — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  877. The last few occurrences of integrable_cong — paulson <lp15@cam.ac.uk> / hgweb
  878. Tidying/removal of obsolete material — paulson <lp15@cam.ac.uk> / hgweb
  879. Fixed a use of Bochner_Integration.integrable_cong — paulson <lp15@cam.ac.uk> / hgweb
  880. fixes for compatibility with renamed / new lemmas — paulson <lp15@cam.ac.uk> / hgweb
  881. Tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
  882. A tiny bit of reorganisation — paulson <lp15@cam.ac.uk> / hgweb
  883. the last "simp/auto" problems — paulson <lp15@cam.ac.uk> / hgweb
  884. corrected all "bysimp" — paulson <lp15@cam.ac.uk> / hgweb
  885. Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.3gPj1U — paulson <lp15@cam.ac.uk> / hgweb
  886. Tidied auto/simp with null arguments — paulson <lp15@cam.ac.uk> / hgweb
  887. merged — nipkow / hgweb
  888. comleted single loop refinement — nipkow / hgweb
  889. minor adjustments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  890. metadata — user9716869 <user9716869@gmail.com> / hgweb
  891. minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  892. creation and preservation of limits; a variety of auxiliary results and amendments — user9716869 <user9716869@gmail.com> / hgweb
  893. patched a broken proof — paulson <lp15@cam.ac.uk> / hgweb
  894. merged — nipkow / hgweb
  895. single lopp variant refined to lists. — nipkow / hgweb
  896. adjust for isabelle@7095df141819 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  897. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  898. typo fix — paulson <lp15@cam.ac.uk> / hgweb
  899. sitegen for Digit_Expansions — paulson <lp15@cam.ac.uk> / hgweb
  900. New entry Digit_Expansions — paulson <lp15@cam.ac.uk> / hgweb
  901. finally!!!!  Sitegen for Sophomore's Dream — paulson <lp15@cam.ac.uk> / hgweb
  902. merged — paulson / hgweb
  903. Minor corrections to metadata (no "and" between authors' names) — paulson <lp15@cam.ac.uk> / hgweb
  904. Updating the version of Jinja2, as suggested by Manuel — paulson <lp15@cam.ac.uk> / hgweb
  905. merged — paulson / hgweb
  906. updated metadata — paulson <lp15@cam.ac.uk> / hgweb
  907. new entry Sophomores_Dream — paulson <lp15@cam.ac.uk> / hgweb
  908. updated name and email address of Rose Bohrer — Manuel Eberl <manuel@pruvisto.org> / hgweb
  909. sitegen for Clique_and_Monotone_Circuits — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  910. new entry Clique_and_Monotone_Circuits — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  911. metadata and sitegen for Fisher's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  912. new entry: Fisher's Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  913. New entry Multiset_Ordering_NPC — nipkow / hgweb
  914. sitegen for Frequence_Moments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  915. new entry: Frequence_Moments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  916. metadata and sitegen for Prefix_Free_Code_Combinators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  917. new entry: Prefix_Free_Code_Combinators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  918. regen website (some orders are different in python3) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  919. switch sitegen to python3 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  920. sitegen for new entry — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  921. new entry: FOL_Seq_Calc3 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  922. New entry: Dedekind_Real — nipkow / hgweb
  923. New entry Ackermann_not_PR, from distribution — nipkow / hgweb
  924. Cotangent_PFD_Formula sitegen — paulson <lp15@cam.ac.uk> / hgweb
  925. new entry Cotangent_PFD_Formula — paulson <lp15@cam.ac.uk> / hgweb
  926. website for Independence_CH — paulson <lp15@cam.ac.uk> / hgweb
  927. new entry Independence_CH — paulson <lp15@cam.ac.uk> / hgweb
  928. New entry ResiduatedTransitionSystem — nipkow / hgweb
  929. Transitive_Models webpage — paulson <lp15@cam.ac.uk> / hgweb
  930. new entry Transitive_Models — paulson <lp15@cam.ac.uk> / hgweb
  931. updated name and email address of Rose Bohrer — Manuel Eberl <manuel@pruvisto.org> / hgweb
  932. Removal of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
  933. perfectly pointless streamlining — paulson <lp15@cam.ac.uk> / hgweb
  934. More general definition of gcard — paulson <lp15@cam.ac.uk> / hgweb
  935. refined one-loop version further — nipkow / hgweb
  936. tidied up a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  937. A bit of beautification — paulson <lp15@cam.ac.uk> / hgweb
  938. Yet more tidying and streamlining of graph lemmas — paulson <lp15@cam.ac.uk> / hgweb
  939. merged — paulson / hgweb
  940. A few trivial changes — paulson <lp15@cam.ac.uk> / hgweb
  941. Tweaks concerning the versions of Zhao's evolving lecture notes — paulson <lp15@cam.ac.uk> / hgweb
  942. Trying to simplify a bit more — paulson <lp15@cam.ac.uk> / hgweb
  943. More simplification of proofs. Removal of numeric references to Zhao. — paulson <lp15@cam.ac.uk> / hgweb
  944. tidying and simplification — paulson <lp15@cam.ac.uk> / hgweb
  945. merged — paulson / hgweb
  946. More purely cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
  947. moved from AFP to distribution — haftmann / hgweb
  948. tuned syntax — haftmann / hgweb
  949. simplified some proofs and deleted quite a bit of redundant material — paulson <lp15@cam.ac.uk> / hgweb
  950. Shorter proofs and leaner notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  951. Minor updates supplied by the author, mostly connected with a reference to a work by Hilbert, now deleted. — paulson <lp15@cam.ac.uk> / hgweb
  952. Add a construction, using ZFC_in_HOL, of the category of small sets and functions. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  953. Resolve a "Duplicate constant declaration" issue that occurs with "isabelle build -o export_theory". — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  954. avoid side effects on working copy while runnign sessions (generated code is unused) — haftmann / hgweb
  955. clarified formatting, for the sake of scala3; — wenzelm / hgweb
  956. Deleted a few redundant lines — paulson <lp15@cam.ac.uk> / hgweb
  957. Trying to beautify this, but it's still ugly — paulson <lp15@cam.ac.uk> / hgweb
  958. And a bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
  959. more renaming and tidying — paulson <lp15@cam.ac.uk> / hgweb
  960. Alphabetic substitutions — paulson <lp15@cam.ac.uk> / hgweb
  961. Eliminated another finiteness assumption — paulson <lp15@cam.ac.uk> / hgweb
  962. Removal of some needless finiteness assumptions — paulson <lp15@cam.ac.uk> / hgweb
  963. Removed a small amount of redundant material from both Szemerédi and Roth — paulson <lp15@cam.ac.uk> / hgweb
  964. merged — paulson / hgweb
  965. tidied up a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  966. A slightly nicer proof — paulson <lp15@cam.ac.uk> / hgweb
  967. merged — paulson / hgweb
  968. tidied and generalised some proofs using small_eqpoll — paulson <lp15@cam.ac.uk> / hgweb
  969. merged — paulson / hgweb
  970. tidied some proofs — paulson <lp15@cam.ac.uk> / hgweb
  971. Improved handling splitting theorems in the alphabet command — Simon Foster <simon.foster@york.ac.uk> / hgweb
  972. Fixed wrong sign handling in fmul-add — Peter Lammich / hgweb
  973. more count_list lemmas — nipkow / hgweb
  974. more count_list — nipkow / hgweb
  975. merged — nipkow / hgweb
  976. moved some count_list lemmas — nipkow / hgweb
  977. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  978. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  979. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  980. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  981. continue 98838b260ed4 — Frédéric Tuong / hgweb
  982. continue ee01bce2ecca — Frédéric Tuong / hgweb
  983. cancel some part of 11d4567f1b99 — Frédéric Tuong / hgweb
  984. cancel some part of 98838b260ed4 — Frédéric Tuong / hgweb
  985. cancel some part of ada85c62541d — Frédéric Tuong / hgweb
  986. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  987. split locale in two — desharna / hgweb
  988. Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  989. Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  990. added some alternative proofs in Smith_Normal_Form entry — jodivaso / hgweb
  991. The last tranche of material to be moved to the complex analysis libraries — paulson <lp15@cam.ac.uk> / hgweb
  992. Removal of material that has since been added to ZFC_in_HOL.General_Cardinals — paulson <lp15@cam.ac.uk> / hgweb
  993. Deleted nearly 200 lines of unused material — paulson <lp15@cam.ac.uk> / hgweb
  994. A new theorem — paulson <lp15@cam.ac.uk> / hgweb
  995. Clarified code module names. — haftmann / hgweb
  996. removed ancient numeral representation — haftmann / hgweb
  997. restore state of VYDRA_MDL to b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  998. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  999. metadata for Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1000. new entry Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1001. New entry Wetzel's Problem — nipkow / hgweb
  1002. metadata for Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1003. new entry Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1004. metadata for VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1005. new entry VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1006. Backed out changeset c9f94b0ae10e — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1007. Backed out changeset b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1008. metadata update for VYDRA_MDL — mraszyk / hgweb
  1009. New entry: VYDRA_MDL — mraszyk / hgweb
  1010. fixed failing proofs — desharna / hgweb
  1011. New definition of the Aleph operator so that it's defined for all arguments,  not just ordinals — paulson <lp15@cam.ac.uk> / hgweb
  1012. ALEXANDRIA acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
  1013. merged — paulson / hgweb
  1014. New set theory lemmas about cardinality (mainly) — paulson <lp15@cam.ac.uk> / hgweb
  1015. Another attempt for a consolidated terminology. — haftmann / hgweb
  1016. Avoid overaggresive splitting. — haftmann / hgweb
  1017. more lemmas for distribution — haftmann / hgweb
  1018. Avoid overaggresive simplification. — haftmann / hgweb
  1019. some new lemmas — paulson <lp15@cam.ac.uk> / hgweb
  1020. merged — nipkow / hgweb
  1021. More material — nipkow / hgweb
  1022. added idempotent most general unifier — desharna / hgweb
  1023. used same parameter order for locales substitution and substitution — desharna / hgweb
  1024. patched for new/simplified lemmas — paulson <lp15@cam.ac.uk> / hgweb
  1025. Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1026. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1027. avoid conflict with index.html in generated html — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1028. New entry: FO_Theory_Rewriting — nipkow / hgweb
  1029. Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.

    + Remove obsolete e-mail from notification mailing list. — Emin Karayel <me@eminkarayel.de> / hgweb
  1030. Improve proofs for Interpolation_Polynomials_HOL_Algebra.

    Reduced the number of apply scripts used. — Emin Karayel <me@eminkarayel.de> / hgweb
  1031. Correct date. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1032. deleted a lemma that's in the devel library — paulson <lp15@cam.ac.uk> / hgweb
  1033. Cleanup and new results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1034. moved theorems into Matrix.thy — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1035. merge of AFP 2021-1 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1036. New AFP entry: Equivalence_Relation_Enumeration — nipkow / hgweb
  1037. new entry: LP_Duality — nipkow / hgweb
  1038. cosmetic tweaks — paulson <lp15@cam.ac.uk> / hgweb
  1039. sitegen and metadata for Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1040. new entry: Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1041. metadata for Quasi_Borel_Spaces, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1042. new entry: Quasi_Borel_Spaces — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1043. sitegen for FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
  1044. new entry FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
  1045. tweak: corollary that the ln also yields irrational numbers — paulson <lp15@cam.ac.uk> / hgweb
  1046. New entry: Interpolation_Polynomials_HOL_Algebra — nipkow / hgweb
  1047. Finally remembered to run sitegen — paulson <lp15@cam.ac.uk> / hgweb
  1048. Fixed the meta data in the abstract as well — paulson <lp15@cam.ac.uk> / hgweb
  1049. Eliminated the references to SOS (which is no longer used) and changed to the document style to "article". — paulson <lp15@cam.ac.uk> / hgweb
  1050. typo — nipkow / hgweb
  1051. typo — nipkow / hgweb
  1052. New entry Irrationals_From_THEBOOK — nipkow / hgweb
  1053. new entry Median_Method — nipkow / hgweb
  1054. Actuarial Mathematics website — paulson <lp15@cam.ac.uk> / hgweb
  1055. New entry Actuarial_Mathematics — paulson <lp15@cam.ac.uk> / hgweb
  1056. Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1057. Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1058. Fix LaTeX issue. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1059. Qualification required(?) — nipkow / hgweb
  1060. merged — nipkow / hgweb
  1061. more variants of the algorithm — nipkow / hgweb
  1062. Added funding acknowledgments.
    Fixed broken BibTeX citation. — Dominique Unruh <unruh@ut.ee> / hgweb
  1063. Strong completeness for PAL systems. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1064. Cleanup. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1065. Fewer parentheses around turnstile + remove unused lemmas. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1066. Simplify proof of truth lemma. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1067. Notation for `imply` and fewer parenthesis around turnstiles. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1068. Abstract results to shorten proofs. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1069. Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1070. merged — wenzelm / hgweb
  1071. tuned whitespace; — wenzelm / hgweb
  1072. more symbols; — wenzelm / hgweb
  1073. profer bundle lattice_syntax; — wenzelm / hgweb
  1074. prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; — wenzelm / hgweb
  1075. Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1076. avoid hardwired document output; — wenzelm / hgweb
  1077. merged — paulson / hgweb
  1078. deleting the overloading of div and mod, with its attendant ambiguities — paulson <lp15@cam.ac.uk> / hgweb
  1079. replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1080. Removal of a lemma (now in the libraries) and a few tweaks — paulson <lp15@cam.ac.uk> / hgweb
  1081. Tuning. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  1082. merged — paulson / hgweb
  1083. tweaks — paulson <lp15@cam.ac.uk> / hgweb
  1084. merged — paulson / hgweb
  1085. Fixed an inadequate description — paulson <lp15@cam.ac.uk> / hgweb
  1086. tuned — haftmann / hgweb
  1087. mv to distribution — nipkow / hgweb
  1088. by now in distribution — nipkow / hgweb
  1089. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1090. fixed abstract — nipkow / hgweb
  1091. tuned — nipkow / hgweb
  1092. website and metadata for Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1093. new entry: Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1094. sorted ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1095. tuned — nipkow / hgweb
  1096. New entry Knights_Tour — nipkow / hgweb
  1097. more thoroughly replace Michael Foster's e-mail address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1098. metadata and sitegen for Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1099. new entry Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1100. update Michael Forster's email address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1101. metadata and sitegen for Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1102. new entry Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  1103. typo — nipkow / hgweb
  1104. merged — nipkow / hgweb
  1105. New entry Regular_Tree_Relations — nipkow / hgweb
  1106. We DON'T want an output directory — paulson <lp15@cam.ac.uk> / hgweb
  1107. MDP-Algorithms website — paulson <lp15@cam.ac.uk> / hgweb
  1108. new entry MDP-Algorithms — paulson <lp15@cam.ac.uk> / hgweb
  1109. typo — paulson <lp15@cam.ac.uk> / hgweb
  1110. new entry MDP-Rewards — paulson <lp15@cam.ac.uk> / hgweb
  1111. fixed typo — paulson <lp15@cam.ac.uk> / hgweb
  1112. CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  1113. used wfP_imp_asymp from HOL — desharna / hgweb
  1114. simplified proof some more — desharna / hgweb
  1115. simplified proof — desharna / hgweb
  1116. Extended protocol model to support composition of more than two protocols without
    the need of re-labeling them, additional automated checks, tighter integration
    of the stateful protocol model and the automated verification (PSPSP) tool. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
  1117. Tweaked some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
  1118. adapted to new Sledgehammer.run_sledgehammer return type — desharna / hgweb
  1119. Strengthened a lemma — paulson <lp15@cam.ac.uk> / hgweb
  1120. updated the definition of scheme — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  1121. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1122. add change history — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1123. updated 2021-1 release dates -> web — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1124. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1125. ignore generated files — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1126. add 2021-1 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1127. set devel version again — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1128. Added tag Isabelle2021-1 for changeset 11f8b03a88ad — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1129. adjust usage version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1130. set release version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1131. update release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1132. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1133. The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
  1134. The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
  1135. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1136. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1137. new entry Foundation_of_geometry — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1138. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1139. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
  1140. adjust for Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1141. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1142. new entry Simplicial_complexes_and_boolean_functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1143. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
  1144. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1145. adjust to Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1146. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1147. metadata and sitegen for Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1148. added Mathematics/Measure theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1149. new entry: Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1150. New entry: Van_Emde_Boas_Trees — nipkow / hgweb
  1151. New entry: Van_Emde_Boas_Trees — nipkow / hgweb
  1152. metadata and sitegen for SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1153. new entry: SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  1154. Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1155. Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1156. Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1157. Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1158. No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1159. Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1160. Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1161. Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1162. Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1163. In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
  1164. A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
  1165. merged — desharna / hgweb
  1166. generalized standard formula redundancy out of standard redundancy — desharna / hgweb
  1167. merged — wenzelm / hgweb
  1168. discontinued Parse.text; — wenzelm / hgweb
  1169. discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
  1170. weakened locale assumptions: wfP implies asymp — desharna / hgweb
  1171. Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1172. refactored Standard_Redundancy_Criterion to not use ordering type classes — desharna / hgweb
  1173. isabelle update_cartouches; — wenzelm / hgweb
  1174. removed obsolete "extend" operation; — wenzelm / hgweb
  1175. more symbolic latex_output via XML (using YXML within text);
    re-use existing Latex.output_markup; — wenzelm / hgweb
  1176. prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
  1177. tuned signature; — wenzelm / hgweb
  1178. feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  1179. Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1180. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1181. adjust for new tags in Isabelle2021-1-RC4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  1182. fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
  1183. In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
  1184. Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1185. Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1186. Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1187. No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1188. Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1189. Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1190. Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  1191. fixed lemma following Isabelle/c256bba593f3 — desharna / hgweb

#22 (May 2, 2023, 9:49:49 PM)

  1. test — Fabian Huch <huch@in.tum.de> / hgweb

#21 (Nov 27, 2021, 12:37:17 AM)

  1. fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb

#20 (Nov 26, 2021, 6:59:36 PM)

  1. fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb

#19 (Nov 26, 2021, 3:28:15 PM)

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

#18 (Oct 22, 2021, 5:09:13 PM)

  1. modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
  2. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  3. Various tuning that for some reason didn't get merged from my master branch. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  4. A spot of polishing — paulson <lp15@cam.ac.uk> / hgweb
  5. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  6. Update metadata to reflect changes made in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  7. Add a revision note concerning material added in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  8. tuned signature, according to Isabelle/042041c0ebeb; — wenzelm / hgweb
  9. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  10. Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  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. — n.muendler <n.muendler@tum.de> / hgweb
  12. discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. merged — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  15. metadata update for MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  16. fixed a mistake in MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  17. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  18. adjusted Virtual-Substitution from 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  19. merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  20. fixed duplicate "and" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  21. sitegen for Virtual_Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  22. new entry: Virtual Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  23. updated website/email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
  24. modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
  25. modifications in Jinja and DOminance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  26. modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  27. merged — wenzelm / hgweb
  28. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); — wenzelm / hgweb
  29. more accurate treatment of context; — wenzelm / hgweb
  30. more accurate treatment of context; — wenzelm / hgweb
  31. more accurate treatment of context; — wenzelm / hgweb
  32. tuned -- proper names/scopes for contexts; — wenzelm / hgweb
  33. tuned proofs; — wenzelm / hgweb
  34. more accurate treatment of context; — wenzelm / hgweb
  35. more accurate treatment of context; — wenzelm / hgweb
  36. proper antiquotations; — wenzelm / hgweb
  37. tuned messages; — wenzelm / hgweb
  38. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
    tuned whitespace; — wenzelm / hgweb
  39. dead code!? — wenzelm / hgweb
  40. clarified signature, following Isabelle/de4f151c2a34; — wenzelm / hgweb
  41. modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  42. CZH: large limits, generalizations, a variety of minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  43. Simplified a definition — paulson <lp15@cam.ac.uk> / hgweb
  44. modify propa — nanjiang <nanjiang@whu.edu.cn> / hgweb
  45. bit singleton shifts recovered for the sake of backward compatibility — haftmann / hgweb
  46. updated to 7422950f3955 — nipkow / hgweb
  47. merge — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
  48. EPO: simplify proof — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
  49. primer — haftmann / hgweb
  50. more complete simp rules — haftmann / hgweb
  51. more complete simp rules (examples) — haftmann / hgweb
  52. avoid overaggressive contraction of conversions — haftmann / hgweb
  53. slightly more prominence for proof tools; more examples — haftmann / hgweb
  54. ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  55. CTR and ETTS: integration with fd5f62176987 — user9716869 <user9716869@gmail.com> / hgweb
  56. adapted QHLProver to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
  57. adapted to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
  58. adapted to devel — nipkow / hgweb
  59. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  60. Weighted_Path_Order: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  61. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  62. add missing session dependency — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  63. new entry FOL_Axiomatic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  64. regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  65. minor editorial changes for CZH entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  66. New entry Weighted_Path_Order — nipkow / hgweb
  67. fxed metadata (forgot .html) in link — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  68. metadata and sitegen for complex bounded operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  69. new entry: Complex_Bounded_Operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  70. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  71. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; — wenzelm / hgweb
  72. clarified timeout;
    tuned whitespace; — wenzelm / hgweb
  73. hide_lams ~> opaque_lifting; — wenzelm / hgweb
  74. clarified antiquotations; — wenzelm / hgweb
  75. proper inst table; — wenzelm / hgweb
  76. clarified antiquotations; — wenzelm / hgweb
  77. clarified antiquotations; — wenzelm / hgweb
  78. proper inst table; — wenzelm / hgweb
  79. clarified antiquotations; — wenzelm / hgweb
  80. clarified antiquotations; — wenzelm / hgweb
  81. clarified antiquotations; — wenzelm / hgweb
  82. clarified antiquotations; — wenzelm / hgweb
  83. unused; — wenzelm / hgweb
  84. merged — wenzelm / hgweb
  85. clarified antiquotations; — wenzelm / hgweb
  86. proper match against const_name; — wenzelm / hgweb
  87. tuned; — wenzelm / hgweb
  88. tuned; — wenzelm / hgweb
  89. clarified antiquotations; — wenzelm / hgweb
  90. clarified antiquotations; — wenzelm / hgweb
  91. clarified antiquotations; — wenzelm / hgweb
  92. fix(ci): clarified addresses, set proper TLS version; — Fabian Huch <huch@in.tum.de> / hgweb
  93. feat(ci): remove hard-coded address; — Fabian Huch <huch@in.tum.de> / hgweb
  94. feat(SpecCheck/Show) tune pretty printing for environments — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  95. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  96. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  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 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  98. New entry: Dominance_CHK — nipkow / hgweb
  99. Schutz_Spacetime website — paulson <lp15@cam.ac.uk> / hgweb
  100. new entry Schutz_Spacetime — paulson <lp15@cam.ac.uk> / hgweb
  101. metadata for Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  102. new entry Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  103. repaired slip — haftmann / hgweb
  104. feat(SpecCheck) folder renaming, types for tests — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  105. tuned — nipkow / hgweb
  106. mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f; — wenzelm / hgweb
  107. ported Design-Theory from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  108. ported Three-Circles from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  109. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  110. ported Cubic_Quartic_Equations from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  111. merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  112. Cubic_Quartic_Equations sitegen — paulson <lp15@cam.ac.uk> / hgweb
  113. new entry Cubic_Quartic_Equations — paulson <lp15@cam.ac.uk> / hgweb
  114. sitegen for combinatorial design theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  115. new entry: Combinatorial Design Theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  116. sitegen for Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  117. new entry: Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  118. clarified modules, according to Isabelle/534b231ce041; — wenzelm / hgweb
  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); — wenzelm / hgweb
  120. clarified signature, according to Isabelle/d882abae3379; — wenzelm / hgweb
  121. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
  122. tuned signature, according to Isabelle/28a582aa25dd; — wenzelm / hgweb
  123. eliminated Specification.definition', following Isabelle/6876e3d5e362; — wenzelm / hgweb
  124. clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; — wenzelm / hgweb
  125. clarified signature, according to Isabelle/612b7e0d6721; — wenzelm / hgweb
  126. tuned signature, according to Isabelle/839a6e284545; — wenzelm / hgweb
  127. merged — sterraf / hgweb
  128. Backed out changeset ef19e4e58b8c
    restoring old argument order on synthesized formulas — sterraf / hgweb
  129. avoid hardwired document; — wenzelm / hgweb
  130. merged — wenzelm / hgweb
  131. tuned signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  132. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  133. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  134. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  135. simplified, using Isabelle/ML operations; — wenzelm / hgweb
  136. adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; — wenzelm / hgweb
  137. tuned whitespace; — wenzelm / hgweb
  138. more scalable operations; — wenzelm / hgweb
  139. merged — sterraf / hgweb
  140. synthesized formulas have their variables permuted — sterraf / hgweb
  141. merged — paulson / hgweb
  142. fixes for cardinality lemmas — paulson <lp15@cam.ac.uk> / hgweb
  143. proper inst table; — wenzelm / hgweb
  144. Graphic rendering of Relational_Method PDF files refined. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
  145. Entry Relational_Method updated. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
  146. more realistic timeout; — wenzelm / hgweb
  147. clarified signature; — wenzelm / hgweb
  148. follow Isabelle/53e28c438f96; — wenzelm / hgweb
  149. clarified signature, following Isabelle/a3b0fc510705; — wenzelm / hgweb
  150. merged — nipkow / hgweb
  151. tuned — nipkow / hgweb
  152. consolidation of rules for bit operations — haftmann / hgweb
  153. tuned name — nipkow / hgweb
  154. Fix typo — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  155. Tune references

    ... using new name of BD_Security_Compositional — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  156. Remove redundant license — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  157. more realistic timeout: approx. 5min CPU time; — wenzelm / hgweb
  158. cleaning up — nipkow / hgweb
  159. New entry CoSMeDis — nipkow / hgweb
  160. New entry CoSMed — nipkow / hgweb
  161. New entry: BD_Security_Compositional — nipkow / hgweb
  162. New entry: CoCon — nipkow / hgweb
  163. updated to devel — nipkow / hgweb
  164. merge from AFP 2021 — nipkow / hgweb
  165. New entry Fresh_Identifiers — nipkow / hgweb
  166. New entry: Relational_Forests — nipkow / hgweb
  167. cleaning up — nipkow / hgweb
  168. merged — nipkow / hgweb
  169. cleaning up — nipkow / hgweb
  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) — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  171. tuned signature, following Isabelle/069f6b2c5a07; — wenzelm / hgweb
  172. metadata update for MFMC_Countable — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  173. derive rel_pmf characterization from bounded and unbounded MFMC theorem — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  174. merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  175. drop boundedness requirement for the sink — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  176. avoid global tmp file: pointless due to implicit theory export; — wenzelm / hgweb
  177. repaired syntax — haftmann / hgweb
  178. tuned signature, following Isabelle/d030b988d470; — wenzelm / hgweb
  179. generalized gt_rat_sign_change to square-free polynomials — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  180. minor updates to bibliography — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  181. clarified signature; — wenzelm / hgweb
  182. clarified abstract and concrete boolean algebras — haftmann / hgweb
  183. antiquotation for bundles — haftmann / hgweb
  184. simplified hierarchy of type classes for bit operations — haftmann / hgweb
  185. restored executable conversions — haftmann / hgweb
  186. dropped junk — haftmann / hgweb
  187. moved theory Bit_Operations into Main corpus — haftmann / hgweb
  188. organize syntax for word operations in bundles — haftmann / hgweb
  189. more systematic approach for instantiation — haftmann / hgweb
  190. avoid seemingly unused transfer rules — haftmann / hgweb
  191. cleaner presentation of analysis theorems in preliminaries — yonoteam / hgweb
  192. Update to new Epistemic_Logic.thy — Asta Halkjær From <andro.from@gmail.com> / hgweb
  193. Avoid typedefs — Asta Halkjær From <andro.from@gmail.com> / hgweb
  194. Clean: set AFP standard document options — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  195. Clean: re-add to chapter AFP — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  196. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  197. Finitely_Generated_Abelian_Groups website — paulson <lp15@cam.ac.uk> / hgweb
  198. new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
  199. Added Finitely_Generated_Abelian_Groups to metadata — Manuel Eberl <eberlm@in.tum.de> / hgweb
  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. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  201. compile — blanchet / hgweb
  202. more realistic timeout: 50min CPU time; — wenzelm / hgweb
  203. Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending
    on Finitely_Generated_Abelian_Groups — Joseph Thommes <joseph-thommes@gmx.de> / hgweb
  204. new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
  205. remove duplicate entry in metadata — Lars Hupel <lars.hupel@mytum.de> / hgweb
  206. more coherent dependencies — haftmann / hgweb
  207. fix(Regex_Equivalence) update to new SpecCheck version — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  208. operations for symbolic computation of bit operations — haftmann / hgweb
  209. fixed Proof_Strategy_Language following Isabelle/f58108b7a60c — desharna / hgweb
  210. SpecCheck now without _ (Regex_Equivalence is still broken) — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  211. T1 fontenc for new entries — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  212. sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  213. update hide_lams -> opaque_lifting — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  214. merged from afp2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  215. website for SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  216. new entry SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  217. metadata and sitegen for MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  218. new entry: MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  219. sitegen for Public Announcement Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  220. new entry "Public Announcement Logic"
    (and sorted ROOTS + removed duplicate entries in ROOTS) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  221. fixed a messy reference — paulson <lp15@cam.ac.uk> / hgweb
  222. Van_der_Waerden website — paulson <lp15@cam.ac.uk> / hgweb
  223. new entry Van_der_Waerden — paulson <lp15@cam.ac.uk> / hgweb
  224. New entry IMP_Compiler — nipkow / hgweb
  225. Removal of unintended files — Susannah Mansky <susannahej@gmail.com> / hgweb
  226. Hidden.thy to Isar — Susannah Mansky <susannahej@gmail.com> / hgweb
  227. merged — desharna / hgweb
  228. renamed hide_lams opaque_lifting — desharna / hgweb
  229. merged — Fabian Huch <huch@in.tum.de> / hgweb
  230. changed to opaque_lifiting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
  231. changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb

#17 (Jul 8, 2021, 12:46:00 PM)

  1. jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
  2. Added missing Public_Announcement_Logic to ROOTS file — Manuel Eberl <eberlm@in.tum.de> / hgweb
  3. More Support on Clean Syntax, Basic Lens Support, New Examples. — Burkhart Wolff <wolff@lri.fr> / hgweb
  4. finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb
  5. arg -> Arg: the last holdout — paulson <lp15@cam.ac.uk> / hgweb
  6. merged — paulson / hgweb
  7. arg -> Arg — paulson <lp15@cam.ac.uk> / hgweb
  8. Add entry public announcement logic — Asta Halkjær From <andro.from@gmail.com> / hgweb
  9. merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  10. adapt to changes in HOL-Library.Cardinality — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  11. Added Approximation_Algorithm for Center_Selection — nipkow / hgweb
  12. proved conditional completeness of compilation — desharna / hgweb
  13. fixed typos — nipkow / hgweb
  14. more word cleanup — haftmann / hgweb
  15. more default simp rules — haftmann / hgweb
  16. some word streamlining — haftmann / hgweb
  17. made consistent again — haftmann / hgweb
  18. Fixed entry name for theories in sub-directory — Fabian Huch <huch@in.tum.de> / hgweb