Library of Formalized Mathematics for Isabelle/Isar (ZF Logic) - News
posted by slawekk, Tue 30 Jun 2009 08:49:33 PM UTC - 0 replies
This version adds a theory on topological groups.
posted by slawekk, Wed 18 Feb 2009 01:33:17 AM UTC - 0 replies
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.
posted by slawekk, Thu 18 Dec 2008 11:15:07 PM UTC - 0 replies
About 50 new theorems, mostly related to folding commutative semigroup operations over finite sets.
posted by slawekk, Mon 22 Sep 2008 01:01:30 AM UTC - 0 replies
This version adds about 50 new facts leading to the theorem that every two linearly ordered finite sets are order isomorphic and the isomorphism is unique.
posted by slawekk, Sat 28 Jun 2008 09:15:48 PM UTC - 0 replies
This version updates IsarMathLib to Isabelle 2008. Two theories on direct product and order on natural numbers have been added. This version of IsarMathLib distribution contains the source of tiddlyisar - the tool for generating TiddlyWiki markup from IsarMathLib theories.
posted by slawekk, Tue 15 Apr 2008 12:38:56 AM UTC - 0 replies
This version is a small update to synchronize with the Tiddly Formal Math Site.
posted by slawekk, Mon 31 Dec 2007 12:28:27 AM UTC - 0 replies
IsarMathLib has been updated to Isabelle 2007. Added a new theory file Fold_ZF.thy about folding lists in set theory and rewrote the Semgroup_ZF.thy to be based on Fold_ZF.
posted by slawekk, Mon 29 Oct 2007 01:46:13 AM UTC - 0 replies
This release is a small update to synchronize with the Formalized Mathematics blog.
posted by slawekk, Sat 29 Sep 2007 04:26:06 PM UTC - 0 replies
The material added in version 1.6.0 is mostly about finite sequences (a.k.a. lists) and operations on them: concatenation, appending an element, discarding the first or last element and folding with a binary operation. This last notion is studied in the new Semigroup_ZF.thy theory where we prove some properties of products of finite sequences of semigroup elements.
posted by slawekk, Mon 16 Jul 2007 05:28:02 PM UTC - 0 replies
Added some material on sequences defined by induction and about a 100 translated Metamath proofs. The parser for Metamath ZF formulas has been rewritten and is based on Parsec now.
[Submit News]
[30 news in archive]

