[isabelle] library of proofs for Isabelle's ZF logic

Some time ago I started a project on the savannah.org
server aimed at writing a library of formalized
mathematics for the Isabelle's ZF logic. It currently
features about 1200 theorems about general topology,
algebra (groups, rings and fields) and a construction
of real numbers as classes of integer almost
All proofs are written in Isar with emphasis on

Everyone who likes to write machine verifiable proofs
is invited to join the project. Please see the details

Slawomir Kolodynski

Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.