Starting from version 1.12.0 (May 2020) IsarMathLib development has moved to its GitHub repository at https://github.com/SKolodynski/IsarMathLib.
This version updates IsarMathLib for Isabelle2016.
This is a maintenance release to update the project for Isabelle 2014.
10 new theory files with 155 new theorems have been contributed by Daniel de la Concepción Sáez. The first theory contributed by Daniel, Topology_ZF_4 (included in the 1.8.0 release) is now presented on isarmathlib.org
A new Topology_ZF_3 theory about product topologies has been added.
I released version 1.7.2. It adds about 50 lemmas mostly in group theory and topology, leading to a characterization of closure in topological groups in terms of neighborhoods of zero.
A couple of theorems in topology and algebra added, leading to some amusing conclusions about the empty set.
I released version 1.7.0 of IsarMathLib. This version adds formalized mathematics contributed by Victor Porton, see theories Generalization_ZF.thy and NatGenIntEx_ZF.thy.
This version adds a theory on topological groups.
This version contains a tool that parses IsarMathLib theories (except those translated form Metamath) and produces HTML files for web presentation. All IsarMathLib theories are now presented on the FomalMath.org site. There is no new formalized mathematics in this release.
About 50 new theorems, mostly related to folding commutative semigroup operations over finite sets.
This version adds about 50 new facts leading to the theorem that every two linearly ordered finite sets are order isomorphic and the isomorphism is unique.
This version updates IsarMathLib to Isabelle 2008. Two theories on direct product and order on natural numbers have been added. This version of IsarMathLib distribution contains the source of tiddlyisar - the tool for generating TiddlyWiki markup from IsarMathLib theories.
This version is a small update to synchronize with the Tiddly Formal Math Site.
IsarMathLib has been updated to Isabelle 2007. Added a new theory file Fold_ZF.thy about folding lists in set theory and rewrote the Semgroup_ZF.thy to be based on Fold_ZF.
This release is a small update to synchronize with the Formalized Mathematics blog.
The material added in version 1.6.0 is mostly about finite sequences (a.k.a. lists) and operations on them: concatenation, appending an element, discarding the first or last element and folding with a binary operation. This last notion is studied in the new Semigroup_ZF.thy theory where we prove some properties of products of finite sequences of semigroup elements.
Added some material on sequences defined by induction and about a 100 translated Metamath proofs. The parser for Metamath ZF formulas has been rewritten and is based on Parsec now.
It seems that there are problems with downloading the recent IsarMathLib releases from the project download page. Before this is is fixed the latest IsarMathLib release can be downloaded from http://www.skokodyn.com/isarmathlib/.
Added 200 Metamath proofs. The translation tool got improved and now features a parser for Metamath ZF formulas.