  Alonzo is a practice-oriented classical higher-order logic that extends
first-order logic and that admits undefined expressions. Named in honor of
Alonzo Church, Alonzo is based on Church's type theory, Church's formulation of
simple type theory. The little theories method is a method for formalizing
mathematical knowledge as a network of theories called a theory graph
consisting of theories as nodes and theory morphisms as directed edges. The
development of a mathematical topic is done in the "little theory" in the
theory graph that has the most convenient level of abstraction and the most
convenient vocabulary, and then the definitions and theorems produced in the
development are transported, as needed, to other theories via the theory
morphisms in the theory graph. The purpose of this paper is to illustrate how a
body of mathematical knowledge can be formalized in Alonzo using the little
theories method. This is done by formalizing monoid theory -- the body of
mathematical knowledge about monoids -- in Alonzo.
