This is an unofficial reimagining of the Archive of Formal Proofs
Mini MLby Wolfgang Naraschewski and Tobias Nipkow