We demonstrate how to use the proof assistant Isabelle/HOL to obtain machine-checked proofs of two fundamental theorems in the double-pushout approach to graph transformation: the uniqueness of derivations up to isomorphism and the so-called Church-Rosser theorem. The first result involves proving the uniqueness of pushout complements, first established by Rosen in 1975. The second result formalises Ehrig’s and Kreowski’s proof of 1976 that parallelly independent direct derivations can be interchanged to obtain derivations ending in a common graph. We also show how to overcome Isabelle’s limitation that graphs in locales must have nodes and edges of pre-defined types.