  We formalise and mechanise a construtive, proof theoretic proof of Craig's
Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma
statements both formally and informally. We also transcribe informally the
formal proofs. We detail the main features of our mechanisation, such as the
formalisation of binding for first order formulae. We also give some
applications of Craig's Interpolation Theorem.
