This is an unofficial reimagining of the Archive of Formal Proofs
Weight-Balanced Treesby Tobias Nipkow and Stefan Dirix