@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"
}