Library of Formalized Mathematics for Isabelle/Isar (ZF Logic) - News
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 https://github.com/SKolodynski/IsarMathLib.
posted by slawekk, Sat 12 Mar 2016 11:21:34 AM UTC
This version updates IsarMathLib for Isabelle2016.
posted by slawekk, Mon 20 Oct 2014 06:36:14 PM UTC
This is a maintenance release to update the project for Isabelle 2014.
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 isarmathlib.org
posted by slawekk, Wed 27 Jun 2012 05:38:06 PM UTC
A new Topology_ZF_3 theory about product topologies has been added.
posted by slawekk, Sat 23 Jul 2011 06:42:09 PM UTC
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
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
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.
posted by slawekk, Tue 30 Jun 2009 08:49:33 PM UTC
This version adds a theory on topological groups.
posted by slawekk, Wed 18 Feb 2009 01:33:17 AM UTC
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.
Powered by Savane 3.14-8aba.
Corresponding source code