An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation by Salomon Sickert May 08