A machine-checked proof of the odd order theorem

Published in In the proceedings of International Conference on Interactive Theorem Proving, 2013