The concept of locales for Isabelle enables local definition and assumption for interactive mechanical proofs. Furthermore,
dependent types are constructed in Isabelle/HOL for first class representation of structure. These two concepts are introduced
briefly. Although each of them has proved useful in itself, their real power lies in combination. This paper illustrates by
examples from abstract algebra how this combination works and argues that it enables modular reasoning.