This is an unofficial reimagining of the Archive of Formal Proofs
The Jordan-Hölder Theoremby Jakob von Raumer
Secondary Sylow Theoremsby Jakob von Raumer