I will describe how standard proofs about the lambda-calculus can be formalised in Isabelle/HOL using a variant of Pitts' nominal logic work. I will first present an inductive definition for alpha-equated lambda-terms (involving names) and then a strong induction principle, which looks very much like the Barendregt variable convention. The technical novelty of my work is that it is compatible with the axiom-of-choice and therefore can be based on standard set-theory (unlike earlier nominal logic work by Pitts' at al).