[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
homomorphisms. 
All proofs are written in Isar with emphasis on
readability. 

Everyone who likes to write machine verifiable proofs
is invited to join the project. Please see the details
at
http://www.nongnu.org/isarmathlib/. 

Slawomir Kolodynski

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com 





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