  Combinatorial design theory studies set systems with certain balance and
symmetry properties and has applications to computer science and elsewhere.
This paper presents a modular approach to formalising designs for the first
time using Isabelle and assesses the usability of a locale-centric approach to
formalisations of mathematical structures. We demonstrate how locales can be
used to specify numerous types of designs and their hierarchy. The resulting
library, which is concise and adaptable, includes formal definitions and proofs
for many key properties, operations, and theorems on the construction and
existence of designs.
