@TechReport{Brotherston:01,
author = "James Brotherston",
title = "Formalising Proofs in {I}sabelle/{HOL} of Equational Properties for the
{$\lambda$}-Calculus Using One-Sorted Variable Names",
institution = "University of Edinburgh",
month = "June",
year = 2001,
note = "Honours dissertation: BSc(Hons) Computer Science {\&} Mathematics"
}