http://www.andrew.cmu.edu/user/avigad/
This is an unofficial reimagining of the Archive of Formal Proofs
Bondy's Theoremby Jeremy Avigad and Stefan Hetzl