Merge/jrh13 master 20260825 - #16

Open

tanyongkiam wants to merge 17 commits into

merge/jrh13-master-20260825

Commits on May 18, 2026

Extended the ring theory library with material on squarefree elements,
jrh13
committed
dd72de9
printer.ml: factor pp_print_term special-form chain into separate functions; add printer_tests (#178)

aqjune-aws
and
claude
authored
b1e9a98

Commits on May 19, 2026

make_checkpoint.py: detect OCaml exceptions during loading (#175)
jargh
authored
43ae32d
Bump python-multipart from 0.0.24 to 0.0.27 in /mcp (#176)
dependabot[bot]
authored
9b510bc

Commits on Jun 2, 2026

Insert space before colon when printing typed symbolic names (#180)

authored
1d2630a

Commits on Jun 4, 2026

pa_j: accept camlp5 8.05 for OCaml 5.4 (#181)
mkannwischer
authored
6c23212
Bump idna from 3.11 to 3.15 in /mcp (#179)
dependabot[bot]
authored
5e62421

Commits on Jun 7, 2026

Added a general "Borel sets of a topological space" theory,
jrh13
committed
36b5225

Commits on Jun 8, 2026

Substantially extended the probability theory library. The main themes
jrh13
committed
87433ef

Commits on Jun 9, 2026

Extended the ring theory library with the Hilbert Basis Theorem for
jrh13
committed
924faf0

Commits on Jul 10, 2026

nets.ml: speed up discrimination-net lookup (#183)

aqjune-aws
and
claude
authored
b19af69

Commits on Jul 14, 2026

Commits on Aug 3, 2026

Added two proof developments involving hypergeometric sums, both
jrh13
committed
6868f3c

Commits on Aug 10, 2026

Added a new subdirectory Autoformalization as a home for miscellaneous
jrh13
committed
9bcbb42

Commits on Aug 17, 2026

Added autoformalized proofs of Carleson's theorem and the 15 theorem.
jrh13
committed
4334778

Commits on Aug 25, 2026

Merge jrh13/hol-light master
tanyongkiam
committed
c093a4c