We give mechanised proofs of Craig interpolation for a Display Calculus for 
classical propositional logic.

We discuss the difficulties caused by various rules, such as the
binary logical introduction rules in their additive and multiplicative forms,
and the weakening and unit weakening rules.

We discuss the differences between our proofs and those of 
Brotherston and Gor\'e, differences motivated by the ease of formalising 
the definitions used in intermediate lemmas,
and we detail how we proved the more difficult cases.
In particular, for the weakening rules and the multiplicative binary logical
introduction rules, we expressed these rules as composition of other rules,
which we describe.

We discuss the value for this work of
using a prover with a programmable user interface
(in our case, Isabelle with its Standard ML interface).