Version 1.35.0

• Updated for Isabelle2025-1
• Uniformities and pseudometrics
• The notions of "countable" and "enumerable" in ZF

Version 1.34.0

• finished the proof that the uniformities on a nonempty set, ordered by inclusion form a complete lattice
• edited IntModule_ZF to present at the isarmathlib.org site

Version 1.33.0

• ultrafilters, ultraproducts, internal sets, hypernatural numbers
• least upper bound of a set of uniformities

Version 1.32.0

• update to Isabelle2025
• uniformity defined by a set of (ordered loop valued) pseudometrics

Version 1.31.0

uniform structure on an ordered loop valued pseudometric space

Version 1.30.0

• Modules: linear combinations, linear dependency, submodules, spans, Z-modules
• Update to Isabelle2024

Version 1.29.0

• New theory files on modules and vector spaces
• Ring_ZF_2 and Ring_ZF_3 edited for isarmathlib.org

Version 1.28.1

IsarMathLib has been updated for Isabelle2023.
Topology_ZF_8 and Group_ZF_5 added to isarmathlib.org.

Version 1.28.0

Added the binomial theorem for commutative rings.

Version 1.27.0

• Ring theory and Zariski topology: reaches the result that the spectrum of a quotient ring is homeomorphic to a closed subspace of the spectrum of the original ring .
• A new theory on Finite State Machines. Reaches a proof that non-deterministic finite state automata determine the same languages as deterministic finite state automata. Also includes results on operations closed for regular languages.