Library of Formalized Mathematics for Isabelle/Isar (ZF Logic) - Summary
This project is not part of the GNU Project.
The goal of the project is to create a library of formalized mathematics, similar to the Mizar Mathematical Library, but written for the Isabelle/Isar theorem prover (ZF logic).
Registration Date: Wed 23 Mar 2005 11:45:13 PM UTC
License: Modified BSD License
Development Status: 4 - Beta
posted by slawekk, Tue 30 Jun 2009 08:49:33 PM UTC - 0 replies
This version adds a theory on topological groups.
posted by slawekk, Wed 18 Feb 2009 01:33:17 AM UTC - 0 replies
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.
posted by slawekk, Thu 18 Dec 2008 11:15:07 PM UTC - 0 replies
About 50 new theorems, mostly related to folding commutative semigroup operations over finite sets.
posted by slawekk, Mon 22 Sep 2008 01:01:30 AM UTC - 0 replies
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.
[Submit News]
[30 news in archive]


