mainLibrary of Formalized Mathematics for Isabelle/Isar (ZF Logic) - Summary

Membership Info
Project Admin:
3 active members

Group identification
Id: #7455
System Name: isarmathlib
Name: Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Group Type: non-GNU software and documentation

Search in this Group


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


Latest News rss feed
Version 1.9.4 released
     posted by slawekk, Sat 12 Mar 2016 11:21:34 AM UTC - 0 replies

This version updates IsarMathLib for Isabelle2016.

Version 1.9.2 released
     posted by slawekk, Mon 20 Oct 2014 06:36:14 PM UTC - 0 replies

This is a maintenance release to update the project for Isabelle 2014.

Version 1.9.0 released
     posted by slawekk, Mon 22 Jul 2013 05:14:22 PM UTC - 0 replies

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

Version 1.7.4 released
     posted by slawekk, Wed 27 Jun 2012 05:38:06 PM UTC - 0 replies

A new Topology_ZF_3 theory about product topologies has been added.

[Submit News]
[37 news in archive]

Back to the top

Powered by Savane 3.1-cleanup1