This is an unofficial reimagining of the Archive of Formal Proofs
AVL Treesby Tobias Nipkow and Cornelia Pusch