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, Wed 27 Jun 2012 05:38:06 PM UTC - 0 replies
A new Topology_ZF_3 theory about product topologies has been added.
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.
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.
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]



