Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal proofs,
especially in proofs by structural and rule induction. In two talks
I will describe a technique for formalising in Isabelle/HOL standard
"paper"-proofs about the lambda-calculus. For this I will present an
inductive definition for alpha-equated lambda-terms and strong
induction principles that have the variable convention already built
in. The aim of this work is to provide all proving technologies
necessary for reasoning conveniently about the lambda-calculus and
programming languages.