Master's practical course, Master's thesis, or IDP

The purpose of this project is to add various missing bits of group theory to HOL-Algebra, with a particular focus on finite groups. Topics of interest include:

Prerequisites:
Experience with Isabelle/HOL is required. Knowledge of basic group theory is recommended. Experience with locales or even HOL-Algebra itself would be helpful, but is not required.
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]