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

 
 
Show feedback again
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 & documentation

Search in this Group

in
   

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 
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.

IsarMathLib version 1.7.2 released
     posted by slawekk, Sat 23 Jul 2011 06:42:09 PM UTC - 0 replies

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.

Version 1.7.1 released
     posted by slawekk, Mon 09 May 2011 12:55:19 PM UTC - 0 replies

A couple of theorems in topology and algebra added, leading to some amusing conclusions about the empty set.

Version 1.7.0 released
     posted by slawekk, Sun 13 Feb 2011 09:44:08 AM UTC - 0 replies

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.


[Submit News]
[34 news in archive]
Show feedback again

Back to the top


Powered by Savane 3.1-cleanup