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

Membership Info
Group 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 group 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
Move to GitHub
     posted by slawekk, Tue 05 May 2020 04:25:05 PM UTC

Starting from version 1.12.0 (May 2020) IsarMathLib development has moved to its GitHub repository at

Version 1.9.4 released
     posted by slawekk, Sat 12 Mar 2016 11:21:34 AM UTC

This version updates IsarMathLib for Isabelle2016.

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

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

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

Quick Overview
 Memberlist (3 members)

Communication Tools
 Mailing Lists (2 public mailing lists)

Development Tools
 Task Manager (open items: 0, total: 0)
 Patch Manager (open items: 0, total: 0)

Back to the top

Powered by Savane 3.13-a854.
Corresponding source code